avoid declaring options twice

This can happen in a coq instance handling multiple files, eg vscoq
LPCIC · Jan 8, 2024 · be04179 · be04179
1 parent 6d94efa
commit be04179
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
@@ -42,8 +42,10 @@ Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
     all-options Options,
-    std.forall Options (x\ sigma L\ x L, 
-      coq.option.add L (coq.option.bool ff) ff).
+    std.forall Options (x\ sigma L\ x L,
+      if (coq.option.available? L _)
+         true
+         (coq.option.add L (coq.option.bool ff) ff)).
 }}.
 Elpi Typecheck.