Merge PR#696: Trunk+cleanup constr of global

4 files changed, 53 insertions, 48 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 29cde4d3d4..87e7e50ec2 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -211,7 +211,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
-	| None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c))
+	| None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
       in 
       Obligations.check_evars env evd;
       let obls, _, c, cty = 
@@ -907,23 +907,26 @@ let fixsub_module = subtac_dir @ ["Wf"]
 let tactics_module = subtac_dir @ ["Tactics"]
 
 let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant  dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s)
+let init_constant  dir s evdref =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref)
+                                                (Coqlib.coq_reference "Command" dir s)
+  in evdref := Sigma.to_evar_map sigma; c
 
 let make_ref l s = init_reference l s
 let fix_proto = init_constant tactics_module "fix_proto"
 let fix_sub_ref = make_ref fixsub_module "Fix_sub"
 let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset name typ prop =
+let mkSubset evdref name typ prop =
   let open EConstr in
-  mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
+  mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
 let sigT = Lazy.from_fun build_sigma_type
 
 let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
-let rec telescope l =
+let rec telescope evdref l =
   let open EConstr in
   let open Vars in
   match l with
@@ -935,10 +938,8 @@ let rec telescope l =
 	  (fun (ty, tys, (k, constr)) decl ->
             let t = RelDecl.get_type decl in
             let pred = mkLambda (RelDecl.get_name decl, t, ty) in
-	    let ty = Universes.constr_of_global (Lazy.force sigT).typ in
-	    let ty = EConstr.of_constr ty in
-	    let intro = Universes.constr_of_global (Lazy.force sigT).intro in
-	    let intro = EConstr.of_constr intro in
+	    let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
+	    let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
 	    let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
 	      (sigty, pred :: tys, (succ k, intro)))
@@ -947,17 +948,15 @@ let rec telescope l =
       let (last, subst) = List.fold_right2
         (fun pred decl (prev, subst) ->
           let t = RelDecl.get_type decl in
-	  let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
-	  let p1 = EConstr.of_constr p1 in
-	  let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
-	  let p2 = EConstr.of_constr p2 in
+	  let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
+	  let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
 	  let proj1 = applist (p1, [t; pred; prev]) in
 	  let proj2 = applist (p2, [t; pred; prev]) in
 	    (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
 	(List.rev tys) tl (mkRel 1, [])
       in ty, (LocalDef (n, last, t) :: subst), constr
 
-  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
       ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
@@ -976,7 +975,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let top_env = push_rel_context binders_rel env in
   let top_arity = interp_type_evars top_env evdref arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
-  let argtyp, letbinders, make = telescope binders_rel in
+  let argtyp, letbinders, make = telescope evdref binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
@@ -1004,7 +1003,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       it_mkLambda_or_LetIn measure letbinders,
       it_mkLambda_or_LetIn measure binders
     in
-    let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+    let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
     let relargty = EConstr.of_constr relargty in
     let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
     let wf_rel_fun x y =
@@ -1012,15 +1011,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
  		     subst1 y measure_body |])
     in wf_rel, wf_rel_fun, measure
   in
-  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
+  let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
   let wfarg len = LocalAssum (Name argid',
-                              mkSubset (Name argid') argtyp
+                              mkSubset evdref (Name argid') argtyp
 				       (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
-  let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
+  let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
   let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1033,7 +1032,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
+    let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
@@ -1059,7 +1058,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let def =
-    mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
+    mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
 	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
@@ -1075,12 +1074,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
       let hook l gr _ = 
-	let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
+	let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ty = EConstr.Unsafe.to_constr ty in
 	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
+	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -1097,10 +1096,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   let hook = Lemmas.mk_hook hook in
-  let fullcoqc = Evarutil.nf_evar !evdref def in
-  let fullctyp = Evarutil.nf_evar !evdref typ in
-  let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
-  let fullctyp = EConstr.Unsafe.to_constr fullctyp in
+  let fullcoqc = EConstr.to_constr !evdref def in
+  let fullctyp = EConstr.to_constr !evdref typ in
   Obligations.check_evars env !evdref;
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
@@ -1143,7 +1140,7 @@ let interp_recursive isfix fixl notations =
 	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
 	   let fixprot =
 	     try 
-	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
+	       let app = mkApp (fix_proto evdref, [|sort; t|]) in
 		 Typing.e_solve_evars env evdref app
 	     with e  when CErrors.noncritical e -> t
 	   in
@@ -1303,9 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns =
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
+      EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
     and typ =
-      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
+      EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
     in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index f57b1bba01..a678d20bba 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -453,11 +453,19 @@ let fold_left' f = function
     [] -> invalid_arg "fold_left'"
   | hd :: tl -> List.fold_left f hd tl
 
+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_and sigma = new_global sigma (Coqlib.build_coq_and ())
+let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ())
+             
 let build_combined_scheme env schemes =
-  let defs = List.map (fun cst -> (* FIXME *)
-    let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
-      (c, Typeops.type_of_constant_in env c)) schemes in
-(*   let nschemes = List.length schemes in *)
+  let evdref = ref (Evd.from_env env) in
+  let defs = List.map (fun cst ->
+    let evd, c = Evd.fresh_constant_instance env !evdref cst in
+    evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in
   let find_inductive ty =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
@@ -471,26 +479,27 @@ let build_combined_scheme env schemes =
   let (c, t) = List.hd defs in
   let ctx, ind, nargs = find_inductive t in
   (* Number of clauses, including the predicates quantification *)
-  let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
-  let coqand  = Universes.constr_of_global @@ Coqlib.build_coq_and () in
-  let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in
+  let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
+  let sigma, coqand  = mk_coq_and !evdref in
+  let sigma, coqconj = mk_coq_conj sigma in
+  let () = evdref := sigma in
   let relargs = rel_vect 0 prods in
   let concls = List.rev_map
-    (fun (cst, t) -> (* FIXME *)
+    (fun (cst, t) ->
       mkApp(mkConstU cst, relargs),
       snd (decompose_prod_n prods t)) defs in
   let concl_bod, concl_typ =
     fold_left'
       (fun (accb, acct) (cst, x) ->
-	mkApp (coqconj, [| x; acct; cst; accb |]),
-	mkApp (coqand, [| x; acct |])) concls
+	mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]),
+	mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls
   in
   let ctx, _ =
     list_split_rev_at prods
       (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
-  (body, typ)
+  (!evdref, body, typ)
 
 let do_combined_scheme name schemes =
   let csts =
@@ -501,9 +510,9 @@ let do_combined_scheme name schemes =
                 with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
       schemes
   in
-  let body,typ = build_combined_scheme (Global.env ()) csts in
+  let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
   let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-  ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
+  ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index e5d79fd514..0f559d2bd8 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit
 
 (** Combine a list of schemes into a conjunction of them *)
 
-val build_combined_scheme : env -> constant list -> constr * types
+val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
 
 val do_combined_scheme : Id.t located -> Id.t located list -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 405d37927f..77be7f454a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1765,12 +1765,11 @@ let vernac_locate = let open Feedback in function
 let vernac_register id r =
  if Pfedit.refining () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let t = (Constrintern.global_reference (snd id)) in
-  if not (isConst t) then
+  let kn = Constrintern.global_reference (snd id) in
+  if not (isConstRef kn) then
     user_err Pp.(str "Register inline: a constant is expected");
-  let kn = destConst t in
   match r with
-  | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+  | RegisterInline -> Global.register_inline (destConstRef kn)
 
 (********************)
 (* Proof management *)