[TC] HO unification

_CoqProject

@@ -1,4 +1,6 @@
 -arg -w -arg +elpi.deprecated
+-arg -w -arg -ambiguous-extra-dep
+-arg -w -arg -future-coercion-class-field
 
 -R theories elpi
 -Q examples elpi.examples

_CoqProject.test

@@ -55,3 +55,4 @@ tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
 tests/test_toposort.v
 tests/test_synterp.v
+tests/test_checker.v

apps/NES/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories elpi.apps
 -Q elpi elpi.apps.NES

apps/coercion/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories   elpi.apps
 

apps/derive/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories elpi.apps
 -Q elpi elpi.apps.derive

apps/eltac/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 # Hack to see derive even if it is not installed yet
 -Q ../derive/theories elpi.apps

apps/locker/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories elpi.apps
 -Q elpi elpi.apps.locker

apps/tc/_CoqProject

@@ -2,6 +2,7 @@
 -Q ../../theories elpi
 -I ../../src
 -docroot elpi.apps
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories   elpi.apps.tc
 -R elpi       elpi.apps.tc
@@ -20,3 +21,5 @@ theories/db.v
 theories/add_commands.v
 theories/tc.v
 theories/wip.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/tc/_CoqProject.test

@@ -1,5 +1,8 @@
--arg -w -arg -Not-added
+# -arg -w -arg -Not-added
 -arg -w -arg -TC.hints
+-arg -w -arg -ambiguous-extra-dep
+-arg -w -arg -future-coercion-class-field
+-arg -bt
 
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
@@ -10,8 +13,6 @@
 -R tests    elpi.apps.tc.tests
 -I src
 
-tests/classes_declare.v
-
 # Register (de-)activation
 tests/register/f1.v
 tests/register/f2.v
@@ -21,6 +22,13 @@ tests/hook_test.v
 
 tests/auto_compile.v
 
+tests/test_HO.v
+tests/test_eta.v
+tests/test_unfold.v
+tests/test_coercion.v
+tests/test_tc_declare.v
+tests/test_pending_mode.v
+
 # Import order of instances
 tests/importOrder/sameOrderCommand.v
 tests/importOrder/f1.v

apps/tc/a.elpi

@@ -0,0 +1,7 @@
+:index (0 3)
+pred a o:int, i:list int.
+
+a 3 [3].
+a X [X] :- X = 2.
+
+main :- a X [X], print X.

apps/tc/elpi/alias.elpi

@@ -1,7 +1,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-accumulate base.
+
 
 pred alias i:term, o:term.
 

apps/tc/elpi/base.elpi

@@ -59,4 +59,28 @@ do [].
 do [P|PS] :- P, do PS.
 
 pred do-once i:prop. 
-do-once A :- A, !.
+do-once A :- A, !.
+
+pred if-true i:prop, i:prop.
+if-true A B :- if A B true.
+
+pred if-false i:prop, i:prop.
+if-false A B :- if A true B.
+
+pred std.findall-unary i:(A -> prop), o:list A.
+std.findall-unary P L :-
+  std.findall (P _) V,
+  std.map V (x\y\ P y = x) L.
+
+pred print-repeat-aux i:int, i:string, o:string.
+print-repeat-aux 0 _ S :- coq.say S.
+print-repeat-aux N A S :- N > 0, N1 is N - 1,
+  S' is A ^ S, print-repeat-aux N1 A S'.
+
+pred print-repeat i:int, i:string.
+print-repeat I S :- print-repeat-aux I S "".
+
+pred split-at-not-fatal i:int, i:list A, o:list A, o:list A.
+split-at-not-fatal 0 L [] L :- !.
+split-at-not-fatal N [X|XS] [X|LN] LM :- !, N1 is N - 1, 
+  split-at-not-fatal N1 XS LN LM.