Merge pull request #29 from coq-community/doc

📝 Doc on do-not-fail
coq-community · Jan 19, 2024 · aff92c4 · aff92c4
2 parents 95f083a + 98f9581
commit aff92c4
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/elpi/util.elpi b/elpi/util.elpi
@@ -14,6 +14,10 @@
 % utility predicates
 % -----------------------------------------------------------------------------
 
+% Some of the Coq native predicates raise errors in Elpi, stopping all
+% ongoing computations. Adding a custom flag like do-not-fail gives us an
+% extra catch-all case in the native predicate, when this flag is active,
+% meaning the predicate will just not succeed, instead of raising an error.
 pred do-not-fail.
 :before "term->gref:fail"
 coq.term->gref _ _ :- do-not-fail, !, false.