5 files changed, 27 insertions, 32 deletions
diff --git a/src/PropToBool.v b/src/PropToBool.v
index 7286216..bbe1967 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -243,7 +243,7 @@ Ltac prop2bool_hyps Hs :=
 Section Test.
   Variable A : Type.
 
-  Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+  Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat.
   Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
   Hypothesis uninterpreted_type : forall (a:A), a = a.
   Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
@@ -318,7 +318,7 @@ End MultipleCompDec.
    polymorphism will be removed before *)
 Section Poly.
   Hypothesis basic : forall (A:Type) (l1 l2:list A),
-    length (l1++l2) = length l1 + length l2.
+    length (l1++l2) = (length l1 + length l2)%nat.
   Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
 
   Goal True.
diff --git a/src/configure.sh b/src/configure.sh
index fb265e0..57a4161 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -39,4 +39,6 @@ else
     cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v
     cp ${pre}versions/standard/Tactics_standard.v ${pre}Tactics.v
     coq_makefile -f _CoqProject -o Makefile
+    # work around https://github.com/coq/coq/issues/12603
+    sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile
 fi
diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
index 8abc72c..c57842a 100644
--- a/src/versions/standard/Makefile.local
+++ b/src/versions/standard/Makefile.local
@@ -25,6 +25,10 @@ clean::
 
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
+CAMLPKGS += -package num
+
+merlin-hook::
+	$(HIDE)echo 'PKG num' >> .merlin
 
 %.ml :  %.mll
 	$(CAMLLEX) $<
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 863c921..11dccbf 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -10,9 +10,6 @@
 (**************************************************************************)
 
 
-open Entries
-
-
 (* Constr generation and manipulation *)
 type id = Names.variable
 let mkId = Names.Id.of_string
@@ -50,47 +47,39 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 let pr_constr = pr_constr_env Environ.empty_env
 
 
-let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c ->
+let mkUConst : Constr.t -> Evd.side_effects Declare.proof_entry = fun c ->
   let env = Global.env () in
   let evd = Evd.from_env env in
   let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
-  { Entries.const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
-                                               Safe_typing.empty_private_constants);
-    const_entry_secctx      = None;
-    const_entry_feedback    = None;
-    const_entry_type        = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
-    const_entry_universes   = Evd.univ_entry ~poly:false evd;
-    const_entry_opaque      = false;
-    const_entry_inline_code = false }
+  Declare.definition_entry
+    ~opaque:false
+    ~inline:false
+    ~types:(EConstr.Unsafe.to_constr ty) (* Cannot contain evars since it comes from a Constr.t *)
+    ~univs:(Evd.univ_entry ~poly:false evd)
+    c
 
 let mkTConst c noc ty =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
-  { const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
-                                               Safe_typing.empty_private_constants);
-    const_entry_secctx      = None;
-    const_entry_feedback    = None;
-    const_entry_type        = Some ty;
-    const_entry_universes   = Evd.univ_entry ~poly:false evd;
-    const_entry_opaque      = false;
-    const_entry_inline_code = false }
+  Declare.definition_entry
+    ~opaque:false
+    ~inline:false
+    ~types:ty
+    ~univs:(Evd.univ_entry ~poly:false evd)
+    c
 
 (* TODO : Set -> Type *)
 let declare_new_type t =
-  let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
+  let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional Constr.mkSet [] Glob_term.Explicit (CAst.make t) in
   Constr.mkVar t
 
 let declare_new_variable v constr_t =
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
-  let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
+  let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional constr_t [] Glob_term.Explicit (CAst.make v) in
   Constr.mkVar v
 
 let declare_constant n c =
-  Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
-
+  Declare.declare_constant ~name:n ~kind:(Decls.IsDefinition Decls.Definition) (Declare.DefinitionEntry c)
 
 
 type cast_kind = Constr.cast_kind
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 104f3f9..1a82d96 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr
 val pr_constr_env : Environ.env -> constr -> Pp.t
 val pr_constr : constr -> Pp.t
 
-val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val mkUConst : constr -> Evd.side_effects Declare.proof_entry
+val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry
 val declare_new_type : id -> types
 val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t
 
 type cast_kind
 val vmcast : cast_kind