diff --git a/elpi/coq-elaborator.elpi b/elpi/coq-elaborator.elpi
index 5f2dea227..fc2f97b1a 100644
--- 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
index 4f3a60a6e..d2afd6012 100644
--- 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)