Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.

As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.

12 files changed, 38 insertions, 29 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b740e192a7..c530cbdeac 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -986,7 +986,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
       i*)
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
-  Evd.empty_evar_universe_context
+  Evd.empty
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 41f3a5a8bf..26706321b5 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -278,7 +278,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      (*FIXME*) Evd.empty_evar_universe_context
+      (*FIXME*) Evd.empty
     new_principle_type
       hook
     ;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 832e933a71..e07bce69c9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1079,7 +1079,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_id = mk_correct_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-                 (*FIXME*) Evd.empty_evar_universe_context
+                 (*FIXME*) Evd.empty
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
@@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-                            (*FIXME*) Evd.empty_evar_universe_context
+                            (*FIXME*) Evd.empty
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8014abf651..ca9f995f15 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1250,7 +1250,7 @@ let is_opaque_constant c =
     | Declarations.Undef _ -> true
     | Declarations.Def _ -> false
 
-let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
+let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
   let current_proof_name = get_current_proof_name () in
   let name = match goal_name with
@@ -1276,7 +1276,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
     let lid = ref [] in
     let h_num = ref (-1) in
     Proof_global.discard_all ();
-    build_proof Evd.empty_evar_universe_context
+    build_proof Evd.empty
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENLIST
@@ -1324,7 +1324,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
   Lemmas.start_proof
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
-    ctx gls_type
+    sigma gls_type
     (Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
@@ -1380,7 +1380,10 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    open_new_goal start_proof (Evd.evar_universe_context sigma)
+    let sigma =
+      Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env
+    in
+    open_new_goal start_proof sigma
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
@@ -1416,11 +1419,14 @@ let (com_eqn : int -> Id.t ->
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
     in
     let (evmap, env) = Lemmas.get_current_context() in
+    let evmap =
+      Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env
+    in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
-       (Evd.evar_universe_context evmap)
+       evmap
        equation_lemma_type
        (Lemmas.mk_hook (fun _ _ -> ()));
      ignore (by
@@ -1488,7 +1494,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let ctx = Evd.evar_universe_context evm in
   let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
@@ -1542,5 +1547,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      ctx (Lemmas.mk_hook hook))
+      evm (Lemmas.mk_hook hook))
     ()
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 1b0b2f401b..cb826bedc4 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -25,9 +25,9 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator =
+let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof (Evd.from_env ~ctx (Global.env ())) id str goals terminator;
+  Proof_global.start_proof sigma id str goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -122,7 +122,8 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  start_proof id goal_kind ctx sign typ (fun _ -> ());
+  let evd = Evd.from_env ~ctx Environ.empty_env in
+  start_proof id goal_kind evd sign typ (fun _ -> ());
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index acf809a2b6..d77ab667bc 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -56,7 +56,7 @@ val delete_all_proofs : unit -> unit
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 
 val start_proof :
-  Id.t -> goal_kind -> Evd.evar_universe_context -> named_context_val -> constr ->
+  Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 0bcefc0e6a..560e662a19 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -350,7 +350,7 @@ let universe_proof_terminator compute_guard hook =
           save_anonymous_with_strength proof kind id
       end
 
-let start_proof id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -358,9 +358,9 @@ let start_proof id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind ctx sign c ?init_tac terminator
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = universe_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -368,7 +368,7 @@ let start_proof_univs id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind ctx sign c ?init_tac terminator
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -446,7 +446,7 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  start_proof_with_initialization kind (Evd.evar_universe_context evd) 
+  start_proof_with_initialization kind evd
     recguard thms snl hook
 
 
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index b77413bc9f..1d08b8fcef 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -25,11 +25,11 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types ->
+val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types ->
+val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Proof_global.proof_universes option -> unit declaration_hook) -> unit
 
@@ -38,7 +38,7 @@ val start_proof_com : goal_kind ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_universe_context -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c09a22c310..b55ee7030b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1804,7 +1804,7 @@ let add_morphism_infer glob m n =
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance = build_morphism_signature m in
-  let ctx = Evd.empty_evar_universe_context (*FIXME *) in
+  let evd = Evd.empty (*FIXME *) in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
 				(Entries.ParameterEntry 
@@ -1831,7 +1831,7 @@ let add_morphism_infer glob m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind ctx instance hook;
+	    Lemmas.start_proof instance_id kind evd instance hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4d23a41818..e034d06740 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -295,7 +295,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    else
 	      (Flags.silently 
 	       (fun () ->
-		Lemmas.start_proof id kind (Evd.evar_universe_context evm) termtype
+		Lemmas.start_proof id kind (Evd.from_env ~ctx:(Evd.evar_universe_context evm) Environ.empty_env) termtype
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fb73c5aa81..76ea462c7c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1046,8 +1046,9 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
+    let evd = Evd.from_env ~ctx Environ.empty_env in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
-      ctx (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1081,8 +1082,9 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
+    let evd = Evd.from_env ~ctx Environ.empty_env in
     Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      ctx (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b303533e48..38580882e9 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -798,7 +798,8 @@ let rec solve_obligation prg num tac =
       | [] ->
           let obl = subst_deps_obl obls obl in
           let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
-            Lemmas.start_proof_univs obl.obl_name kind prg.prg_ctx obl.obl_type
+            let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
+            Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type
               (fun ctx' -> Lemmas.mk_hook (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =