Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

9 files changed, 55 insertions, 31 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3fc01c0bc1..1b329dbc4b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,8 +36,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac terminator =
 
 let cook_this_proof p =
   match p with
-  | { Proof_global.id;entries=[constr];persistence } ->
-      (id,(constr,persistence))
+  | { Proof_global.id;entries=[constr];persistence;constraints } ->
+      (id,(constr,constraints,persistence))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof () =
@@ -123,7 +123,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem)
   start_proof id goal_kind sign typ (fun _ -> ());
   try
     let status = by tac in
-    let _,(const,_) = cook_proof () in
+    let _,(const,_,_) = cook_proof () in
     delete_current_proof ();
     const, status, !substref
   with reraise ->
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 877b7c8586..b99bbe8723 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * goal_kind))
+    (Entries.definition_entry * Univ.constraints * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * goal_kind))
+    (Entries.definition_entry * Univ.constraints * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 30b65d0ce9..f2b64fb187 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -53,7 +53,7 @@ val proof : proof ->
 
 val start : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> proof
 val dependent_start : Evd.evar_map -> Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_goals : proof -> (Term.constr * Term.types Univ.in_universe_context_set) list
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f7548b6ca9..c11a26fb2c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,6 +68,7 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
+  constraints : Univ.constraints;
 }
 
 type proof_ending =
@@ -271,7 +272,7 @@ let close_proof ?feedback_id ~now fpl =
   let initial_goals = Proof.initial_goals proof in
   let fpl, univs = Future.split2 fpl in
   let () = if poly || now then ignore (Future.compute univs) in
-  let entries = Future.map2 (fun p (c, t) ->
+  let entries = Future.map2 (fun p (c, (t, octx)) ->
     let compute_univs (usubst, uctx) = 
       let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in
       let compute_c_t (c, eff) =
@@ -290,19 +291,33 @@ let close_proof ?feedback_id ~now fpl =
     let t = Future.chain ~pure:true ans (fun (_, x, _) -> x) in
     let univs = Future.chain ~pure:true ans (fun (_, _, x) -> x) in
     let t = Future.force t in
-    { Entries.
-    const_entry_body = p;
-    const_entry_secctx = section_vars;
-    const_entry_type  = Some t;
-    const_entry_feedback = feedback_id;
-    const_entry_inline_code = false;
-    const_entry_opaque = true;
-    const_entry_universes = univs;
-    const_entry_polymorphic = pi2 strength;
-    const_entry_proj = None}) fpl initial_goals in
-  if now then
-    List.iter (fun x -> ignore(Future.force x.Entries.const_entry_body)) entries;
-  { id = pid; entries = entries; persistence = strength },
+      { Entries.
+	const_entry_body = p;
+	const_entry_secctx = section_vars;
+	const_entry_type  = Some t;
+	const_entry_inline_code = false;
+	const_entry_opaque = true;
+	const_entry_universes = univs;
+        const_entry_feedback = None;
+	const_entry_polymorphic = pi2 strength;
+	const_entry_proj = None}) fpl initial_goals in
+  let globaluctx = 
+    if not poly then
+      List.fold_left (fun acc (c, (t, octx)) -> 
+	Univ.ContextSet.union octx acc)
+	Univ.ContextSet.empty initial_goals
+    else Univ.ContextSet.empty
+  in
+  let _ = 
+    if now then
+      List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries
+  in
+(*  let hook = Option.map (fun f -> 
+    if poly || now then f (Future.join univs) 
+    else f (Univ.LMap.empty,Univ.UContext.empty))
+    hook
+  in*) (* FIXME *)
+  { id = pid; entries = entries; persistence = strength; constraints = Univ.ContextSet.constraints globaluctx },
   Ephemeron.get terminator
 
 type closed_proof_output = Entries.proof_output list * 
@@ -330,8 +345,8 @@ let return_proof () =
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  let goals = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in
-    goals, (subst, ctx)
+  let proofs = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in
+    proofs, (subst, ctx)
 
 let close_future_proof ~feedback_id proof =
   close_proof ~feedback_id ~now:false proof
@@ -493,8 +508,10 @@ let _ =
 
 module V82 = struct
   let get_current_initial_conclusions () =
-    let { pid; strength; proof } = cur_pstate () in
-    pid, (List.map snd (Proof.initial_goals proof), strength)
+  let { pid; strength; proof } = cur_pstate () in
+  let initial = Proof.initial_goals proof in
+  let goals = List.map (fun (o, (c, ctx)) -> c) initial in
+    pid, (goals, strength)
 end
 
 type state = pstate list
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index f10e991eab..6c11ee9b48 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -61,6 +61,8 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
+  constraints : Univ.constraints;
+  (** guards : lemma_possible_guards; *)
 }
 
 type proof_ending =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d0a477431f..291da4a983 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -26,7 +26,7 @@ open Util
 type proofview = Proofview_monad.proofview
 open Proofview_monad
 
-type entry = (Term.constr * Term.types) list
+type entry = (Term.constr * Term.types Univ.in_universe_context_set) list
 
 let proofview p =
   p.comb , p.solution
@@ -42,7 +42,7 @@ let init sigma =
     let (e, _) = Term.destEvar econstr in
     let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in
     let gl = Goal.build e in
-    let entry = (econstr, typ) :: ret in
+    let entry = (econstr, (typ, ctx)) :: ret in
     entry, { solution = new_defs; comb = gl::comb; }
   in
   fun l ->
@@ -52,17 +52,18 @@ let init sigma =
 
 type telescope =
   | TNil
-  | TCons of Environ.env*Term.types*(Term.constr -> telescope)
+  | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope)
 
 let dependent_init =
   let rec aux sigma = function
   | TNil -> [], { solution = sigma; comb = []; }
-  | TCons (env, typ, t) ->
+  | TCons (env, (typ, ctx), t) ->
     let (sigma, econstr ) = Evarutil.new_evar sigma env typ in
+    let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
     let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
-    let entry = (econstr, typ) :: ret in
+    let entry = (econstr, (typ, ctx)) :: ret in
     entry, { solution = sol; comb = gl :: comb; }
   in
   fun sigma t ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index bfb88c897a..dddf9b1c21 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -41,7 +41,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_se
 
 type telescope =
   | TNil
-  | TCons of Environ.env*Term.types*(Term.constr -> telescope)
+  | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope)
 
 (* Like [init], but goals are allowed to be depedenent on one
    another. Dependencies between goals is represented with the type
@@ -57,7 +57,7 @@ val finished : proofview -> bool
 val return : proofview -> Evd.evar_map
 
 val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
+val initial_goals : entry -> (constr * types Univ.in_universe_context_set) list
 val emit_side_effects : Declareops.side_effects -> proofview -> proofview
 
 (*** Focusing operations ***)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2faf18355e..695e8ab6ef 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,6 +75,8 @@ let pf_reduction_of_red_expr gls re c =
   (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
+let pf_eapply f gls x = 
+  on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
 
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 326d14bf69..cd4e796d5b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -54,6 +54,8 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
+val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> 
+  goal sigma -> 'a -> goal sigma * 'b
 val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
   goal sigma -> constr -> constr