No stdlib

builtin-doc/coq-builtin.elpi

@@ -558,8 +558,8 @@ external pred coq.version o:string, o:int, o:int, o:int.
 
 % To make the API more precise we use different data types for the names
 % of global objects.
-% Note: [ctype \"bla\"] is an opaque data type and by convention it is
-% written [@bla].
+% Note: [ctype "bla"] is an opaque data type and by convention it is written
+% [@bla].
 
 % Global constant name
 typeabbrev constant (ctype "constant").

builtin-doc/elpi-builtin.elpi

@@ -449,6 +449,9 @@ pred ignore-failure! i:prop.
 ignore-failure! P :- P, !.
 ignore-failure! _.
 
+pred once i:prop.
+once P :- P, !.
+
 % [assert! C M] takes the first success of C or fails with message M 
 pred assert! i:prop, i:string.
 assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !.

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.

elpi/dune

@@ -1,6 +1,9 @@
 (coq.theory
  (name elpi_elpi) ; FIXME
- (package coq-elpi))
+ (package coq-elpi)
+ (stdlib no)
+ (theories Coq)
+ )
 
 (rule
  (target dummy.v)

examples/dune

@@ -2,6 +2,8 @@
  (package coq-elpi)
  (name elpi_examples)
  (plugins coq-elpi.elpi)
- (theories elpi))
+ (theories elpi Coq)
+ (stdlib no)
+ )
 
 ; (include_subdirs qualified)

examples/example_abs_evars.v

@@ -1,3 +1,4 @@
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 (** Closing a term with holes with binders *)

examples/example_curry_howard_tactics.v

@@ -1,3 +1,4 @@
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 (* Tactics 

examples/example_fuzzer.v

@@ -1,3 +1,4 @@
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 (** Intrinsically typed data type and semantics, from software foundations.
@@ -96,4 +97,4 @@ Elpi Typecheck.
 Elpi fuzz eval eval1.
 
 (* let's print our new, broken, semantics ;-) *)
-Print eval1.
+Print eval1.

examples/example_generalize.v

@@ -1,3 +1,4 @@
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 (** Abstract a term over something, like the generalize tactic *)

examples/example_import_projections.v

@@ -1,3 +1,4 @@
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 (* "import" a record instance by naming it's applied projections *)

examples/example_record_expansion.v

@@ -1,3 +1,4 @@
+From Coq Require Import Datatypes Logic.
 From elpi Require Import elpi.
 
 (**

examples/example_record_to_sigma.v

@@ -1,3 +1,4 @@
+From Coq Require Import Datatypes Logic Specif.
 From elpi Require Import elpi.
 
 (* Define a command to turn records into nested sigma types, suggested

examples/example_reduction_surgery.v

@@ -3,6 +3,7 @@
    from a given module.
 *)
 
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 Elpi Tactic reduce.

examples/example_reflexive_tactic.v

@@ -9,6 +9,7 @@
 
 *)
 
+From Coq Require Import Prelude.
 From elpi Require elpi.
 Require Arith ZArith Psatz List ssreflect.
 

examples/tutorial_coq_elpi_HOAS.v

@@ -45,6 +45,7 @@ HOAS for Gallina
 
 |*)
 
+From Coq Require Import Prelude.  (* .none *)
 From elpi Require Import elpi.  (* .none *)
 
 Elpi Command tutorial_HOAS. (* .none *)

examples/tutorial_coq_elpi_command.v

@@ -44,6 +44,7 @@ Let's create a simple command, called "hello", which prints :e:`"Hello"`
 followed by the arguments we pass to it:
 
 |*)
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 Elpi Command hello.

examples/tutorial_coq_elpi_tactic.v

@@ -55,6 +55,7 @@ Let's define a simple tactic that prints the current goal.
 
 |*)
 
+From Coq Require Import Prelude.
 From elpi Require Import elpi.
 
 Elpi Tactic show.

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)