Merge PR#696: Trunk+cleanup constr of global

3 files changed, 20 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 38c75fcf8..80680e408 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign =
 	   (Some ([], 0, 0, [])) eqnpats pats
 	 in match acc with
 	     None -> c
-	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
-		 (lift_rel_context liftsign sign)
-	       in
-		 conj :: c)
+	    | Some (sign, len, _, c') ->
+               let sigma, conj = mk_coq_and !evdref c' in
+               let sigma, neg = mk_coq_not sigma conj in
+	       let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in
+               evdref := sigma; conj :: c)
       [] prevpatterns
   in match diffs with [] -> None
-    | _ -> Some (mk_coq_and diffs)
+    | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj)
 
 let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
   let i = ref 0 in
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8769c5659..2fa3facb3 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 
-let init_constant  dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s
 let init_reference dir s () = Coqlib.coq_reference  "Program" dir s
 
 let papp evdref r args = 
@@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect"
 let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq"
 let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
 
-let coq_not = init_constant ["Init";"Logic"] "not"
-let coq_and = init_constant ["Init";"Logic"] "and"
+let coq_not = init_reference ["Init";"Logic"] "not"
+let coq_and = init_reference ["Init";"Logic"] "and"
 
-let delayed_force c = EConstr.of_constr (c ())
+let new_global sigma gr =
+  let open Sigma in
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
 
-let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |])
+let mk_coq_not sigma x =
+  let sigma, notc = new_global sigma (coq_not ()) in
+  sigma, EConstr.mkApp (notc, [| x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
   | [] -> invalid_arg "unsafe_fold_right"
 
-let mk_coq_and l =
-  let and_typ = delayed_force coq_and in
-    unsafe_fold_right
+let mk_coq_and sigma l =
+  let sigma, and_typ = new_global sigma (coq_and ()) in
+  sigma, unsafe_fold_right
       (fun c conj ->
 	 EConstr.mkApp (and_typ, [| c ; conj |]))
       l
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 94a7bdcb6..8439b9528 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference
 val coq_JMeq_ind : unit -> global_reference
 val coq_JMeq_refl : unit -> global_reference
 
-val mk_coq_and : constr list -> constr
-val mk_coq_not : constr -> constr
+val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
+val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
 
 (** Polymorphic application of delayed references *)
 val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr