diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v index 26a964cd8..791bfb325 100644 --- a/apps/coercion/theories/coercion.v +++ b/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. }}. diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 84002d453..30a9f6a25 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/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 ->.