Removed stdlib

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.