Merge pull request #886 from Tragicus/indexing

Indexing in coercion and tc

Author: gares

apps/coercion/theories/coercion.v

@@ -10,6 +10,7 @@ Elpi Db coercion.db lp:{{
 % - [Expected] is the type [V] should be coerced to
 % - [Res] is the result (of type [Expected])
 % Be careful not to trigger coercion as this may loop.
+:index(_ _ 10 10)
 pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
 
 }}.

apps/tc/elpi/create_tc_predicate.elpi

@@ -17,11 +17,13 @@ func add-class-gr search-mode, gref ->.
 add-class-gr _ ClassGR :- tc.class ClassGR _ _ _, !. 
 add-class-gr SearchMode ClassGR :-
   std.assert! (coq.TC.class? ClassGR) "Only gref of type classes can be added as new predicates",
-  tc.get-elpi-mode ClassGR EM SM, 
+  tc.get-elpi-mode ClassGR EM SM,
+  if (std.forall EM (m\ sigma a s\ m = pr a s, a = out)) (true) (
+    std.fold EM "" (m\s\r\ sigma a s'\ m = pr a s', if (a = in) (calc (s ^ " 10") r) (calc (s ^ " _") r)) Indexing),
   tc.gref->pred-name ClassGR PredName,
   get-class-locality Locality, 
   Locality => (
-    coq.elpi.add-predicate "tc.db" _ PredName EM,
+    coq.elpi.add-predicate "tc.db" Indexing PredName EM,
     tc.add-tc-db _ _ (tc.class ClassGR PredName SearchMode SM)).
 
 func add-class-str search-mode, string ->.