Proofs now take and return an evar_universe_context, simplifying interfaces

and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.

7 files changed, 61 insertions, 87 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 077057f3cc..d3410ea751 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 hyps c ?init_tac terminator =
+let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof id str goals terminator;
+  Proof_global.start_proof id str ctx goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -118,8 +118,8 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  start_proof id goal_kind sign typ (fun _ -> ());
+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 _ -> ());
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
@@ -130,15 +130,16 @@ let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem)
     delete_current_proof ();
     raise reraise
 
-let build_by_tactic env ?(poly=false) typ tac =
+let build_by_tactic env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
-  let ce, status, univs = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
+  let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
   let ce = Term_typing.handle_side_effects env ce in
-  let cb, se = Future.force ce.const_entry_body in
+  let (cb, ctx), se = Future.force ce.const_entry_body in
   assert(Declareops.side_effects_is_empty se);
-  cb, status, fst univs
+  assert(Univ.ContextSet.is_empty ctx);
+  cb, status, univs
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
@@ -160,7 +161,7 @@ let solve_by_implicit_tactic env sigma evk =
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
       (try
         let (ans, _, _) = 
-	  build_by_tactic env (evi.evar_concl, Evd.universe_context_set sigma) tac in
-        fst ans
+	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
+        ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 615866c6ae..acf809a2b6 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 -> named_context_val -> constr Univ.in_universe_context_set ->
+  Id.t -> goal_kind -> Evd.evar_universe_context -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -148,13 +148,13 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
     tactic. *)
 
 val build_constant_by_tactic :
-  Id.t -> named_context_val -> ?goal_kind:goal_kind ->
-    types Univ.in_universe_context_set -> unit Proofview.tactic -> 
-  Entries.definition_entry * bool * Universes.universe_opt_subst Univ.in_universe_context
+  Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
+  types -> unit Proofview.tactic -> 
+  Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : env -> ?poly:polymorphic -> 
-  types Univ.in_universe_context_set -> unit Proofview.tactic -> 
-  constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst
+val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> 
+  types -> unit Proofview.tactic -> 
+  constr * bool * Evd.evar_universe_context
 
 (** Declare the default tactic to fill implicit arguments *)
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index f2b64fb187..a77b741249 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -51,9 +51,9 @@ val proof : proof ->
 
 (*** General proof functions ***)
 
-val start : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> proof
+val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
 val dependent_start : Evd.evar_map -> Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types Univ.in_universe_context_set) list
+val initial_goals : proof -> (Term.constr * Term.types) 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 7c44f1500d..410335b47e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,7 +63,7 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
+type proof_universes = Evd.evar_universe_context
 
 type proof_object = {
   id : Names.Id.t;
@@ -222,22 +222,22 @@ let disactivate_proof_mode mode =
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
-let start_proof id str goals terminator =
+let start_proof id str ctx goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.start (Evd.from_env (Global.env ())) goals;
+    proof = Proof.start (Evd.from_env ~ctx (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
-let start_dependent_proof id str goals terminator =
+let start_dependent_proof id str ctx goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals;
+    proof = Proof.dependent_start (Evd.from_env ~ctx (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
@@ -269,54 +269,33 @@ let close_proof ?feedback_id ~now fpl =
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let fpl, univs = Future.split2 fpl in
-  let univsubst, make_body =
+  let universes = Future.force univs in
+  let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+    (Evd.evar_universe_context_subst universes) in
+  let make_body =
     if poly || now then
-      let make_usubst (usubst, uctx) =
-	let ctx, subst = 
-	  Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) 
-	in
-	let nf x = 
-	  let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in
-	    Vars.subst_univs_level_constr subst (nf x)
-	in
-	let subst = 
-	  Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst)
-	in
-	let univsubst = (subst, Univ.ContextSet.to_context ctx) in
-	  univsubst, nf
-      in
-      let make_body nf ctx t _octx ((c, _ctx), eff) =
-	let body = nf c and typ = nf t in
+      let make_body t ((c, _ctx), eff) =
+	let body = c and typ = nf t in
 	let used_univs = 
 	  Univ.LSet.union (Universes.universes_of_constr body)
-	    (Universes.universes_of_constr typ)
+	  (Universes.universes_of_constr typ)
 	in
-	let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) used_univs in
-	let p = (body, Univ.ContextSet.empty),eff in
+	let ctx = Evd.evar_universe_context_set universes in
+	let ctx = Universes.restrict_universe_context ctx used_univs in
 	let univs = Univ.ContextSet.to_context ctx in
+	let p = (body, Univ.ContextSet.empty), eff in
 	  (univs, typ), p
-      in
-      let make_body nf ctx t octx p = 
-	Future.split2 (Future.chain ~pure:true p (make_body nf ctx t octx))
-      in
-      let univsubst =
-	Future.chain ~pure:true univs make_usubst
-      in univsubst, make_body
+      in 
+	fun t p ->
+	  Future.split2 (Future.chain ~pure:true p (make_body t))
     else
-      let ctx = 
-	List.fold_left (fun acc (c, (t, octx)) -> 
-	  Univ.ContextSet.union octx acc)
-	  Univ.ContextSet.empty initial_goals
-      in
-      let univs = Univ.ContextSet.to_context ctx in
-      let univsubst = (Univ.LMap.empty, univs) in
-      let make_body nf ctx t octx p = Future.from_val (univs, t), p in
-	Future.from_val (univsubst, fun x -> x), make_body
+      let univs = Evd.evar_context_universe_context universes in
+	fun t p ->
+	  Future.from_val (univs, nf t), p  
   in
-  let univsubst, nf = Future.force univsubst in
   let entries =
-    Future.map2 (fun p (c, (t, octx)) -> 
-      let univstyp, body = make_body nf (snd univsubst) t octx p in
+    Future.map2 (fun p (c, t) -> 
+      let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
 	{ Entries.
 	  const_entry_body = body;
@@ -329,11 +308,10 @@ let close_proof ?feedback_id ~now fpl =
 	  const_entry_polymorphic = poly;
 	  const_entry_proj = false})
       fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength; universes = univsubst },
+  { id = pid; entries = entries; persistence = strength; universes = universes },
   Ephemeron.get terminator
 
-type closed_proof_output = Entries.proof_output list * 
-    Universes.universe_opt_subst Univ.in_universe_context
+type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context
 
 let return_proof () =
   let { proof } = cur_pstate () in
@@ -352,14 +330,12 @@ let return_proof () =
               str"variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.nf_constraints evd in
-  let subst = Evd.universe_subst evd in
-  let ctx = Evd.universe_context_set evd in
   (** 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 proofs = 
-    List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, ctx), eff)) initial_goals in
-    proofs, (subst, Univ.ContextSet.to_context ctx)
+    List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, Univ.ContextSet.empty), eff)) initial_goals in
+    proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
   close_proof ~feedback_id ~now:false proof
@@ -523,7 +499,7 @@ module V82 = struct
   let get_current_initial_conclusions () =
   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
+  let goals = List.map (fun (o, c) -> c) initial in
     pid, (goals, strength)
 end
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 1ad1cebf8c..d5229c5625 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -53,7 +53,7 @@ val give_me_the_proof : unit -> Proof.proof
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Universes.universe_opt_subst Univ.in_universe_context
+type proof_universes = Evd.evar_universe_context
 type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
@@ -78,13 +78,13 @@ type closed_proof = proof_object * proof_terminator
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
 val start_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types Univ.in_universe_context_set) list  ->
+  Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> (Environ.env * Term.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
+  Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> Proofview.telescope  ->
     proof_terminator -> unit
 
 (* Takes a function to add to the exceptions data relative to the
@@ -95,8 +95,7 @@ val close_proof : (exn -> exn) -> closed_proof
  * Both access the current proof state. The formes is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = Entries.proof_output list * 
-    Universes.universe_opt_subst Univ.in_universe_context
+type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context
 
 val return_proof : unit -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t ->
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index eaaa1f7c30..c8983700f9 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 Univ.in_universe_context_set) list
+type entry = (Term.constr * Term.types) list
 
 let proofview p =
   p.comb , p.solution
@@ -36,13 +36,12 @@ let proofview p =
 let init sigma =
   let rec aux = function
   | [] ->  [], { solution = sigma; comb = []; }
-  | (env, (typ,ctx)) :: l ->
+  | (env, typ) :: l ->
     let ret, { solution = sol; comb = comb } = aux l in
     let (new_defs , econstr) = Evarutil.new_evar sol env typ in
     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, ctx)) :: ret in
+    let entry = (econstr, typ) :: ret in
     entry, { solution = new_defs; comb = gl::comb; }
   in
   fun l ->
@@ -52,18 +51,17 @@ let init sigma =
 
 type telescope =
   | TNil
-  | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope)
+  | TCons of Environ.env * Term.types * (Term.constr -> telescope)
 
 let dependent_init =
   let rec aux sigma = function
   | TNil -> [], { solution = sigma; comb = []; }
-  | TCons (env, (typ, ctx), t) ->
+  | TCons (env, typ, 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, ctx)) :: ret in
+    let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; }
   in
   fun sigma t ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index c27e4ba1a9..f959513d42 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -37,11 +37,11 @@ type entry
 
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, creating that many initial goals. *)
-val init : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
 
 type telescope =
   | TNil
-  | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope)
+  | TCons of Environ.env * Term.types * (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 Univ.in_universe_context_set) list
+val initial_goals : entry -> (constr * types) list
 val emit_side_effects : Declareops.side_effects -> proofview -> proofview
 
 (*** Focusing operations ***)