Removed stdlib dependency in a few more pieces

LPCIC · Aug 21, 2024 · 6932ab6 · 6932ab6
1 parent 1359ed2
commit 6932ab6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/elpi/coq-elaborator.elpi b/elpi/coq-elaborator.elpi
@@ -37,13 +37,13 @@ pred propagate-Prop-constraint-inward i:term.
 propagate-Prop-constraint-inward {{ forall x : lp:Ty, lp:(F x) }} :- !,
   @pi-decl `x` Ty x\
     propagate-Prop-constraint-inward (F x).
-propagate-Prop-constraint-inward {{ lp:A /\ lp:B }} :- !,
+propagate-Prop-constraint-inward {{ Logic.and lp:A lp:B }} :- !,
   propagate-Prop-constraint-inward A,
   propagate-Prop-constraint-inward B.
-propagate-Prop-constraint-inward {{ lp:A \/ lp:B }} :- !,
+propagate-Prop-constraint-inward {{ Logic.or lp:A lp:B }} :- !,
   propagate-Prop-constraint-inward A,
   propagate-Prop-constraint-inward B.
-propagate-Prop-constraint-inward {{ ~ lp:A }} :- !,
+propagate-Prop-constraint-inward {{ Logic.not lp:A }} :- !,
   propagate-Prop-constraint-inward A.
 propagate-Prop-constraint-inward (uvar as X) :- !,
   coq.typecheck X {{ Prop }} ok.

diff --git a/theories/dune b/theories/dune
@@ -2,7 +2,9 @@
  (name elpi)
  (package coq-elpi)
  (plugins coq-elpi.elpi)
- (theories elpi_elpi))
+ (theories elpi_elpi Coq)
+ (stdlib no)
+ )
 
 (rule
  (target elpi.v)