Univs: correctly register universe binders for lemmas.

7 files changed, 88 insertions, 58 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 02dbd1fdcb..cbccf00e72 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name
 let get_all_proof_names = Proof_global.get_all_proof_names
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
 
 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 sigma hyps c ?init_tac terminator =
+let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof sigma id str goals terminator;
+  Proof_global.start_proof sigma id ?pl str goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -54,6 +55,9 @@ let set_used_variables l =
 let get_used_variables () =
   Proof_global.get_used_variables ()
 
+let get_universe_binders () =
+  Proof_global.get_universe_binders ()
+
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
   | NoSuchGoal -> Errors.error "No such goal."
@@ -139,7 +143,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
-    const, status, univs
+    const, status, fst univs
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fc521ea432..d0528c9fdf 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -55,8 +55,10 @@ val delete_all_proofs : unit -> unit
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 
+type universe_binders = Id.t Loc.located list
+
 val start_proof :
-  Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -121,6 +123,9 @@ val set_used_variables :
   Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> universe_binders option
+
 (** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c303f486c5..3d60ff217a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,14 +63,14 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
@@ -89,6 +89,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode Ephemeron.key;
+  universe_binders: universe_binders option;
 }
 
 (* The head of [!pstates] is the actual current proof, the other ones are
@@ -226,7 +227,7 @@ let disactivate_proof_mode mode =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints). *)
-let start_proof sigma id str goals terminator =
+let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -234,10 +235,11 @@ let start_proof sigma id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
-let start_dependent_proof id str goals terminator =
+let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -245,10 +247,12 @@ let start_dependent_proof id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
+let get_universe_binders () = (cur_pstate ()).universe_binders
 
 let proof_using_auto_clear = ref true
 let _ = Goptions.declare_bool_option
@@ -296,7 +300,8 @@ let get_open_goals () =
     List.length shelf
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
-  let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+    cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
@@ -362,8 +367,13 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
 	  const_entry_polymorphic = poly})
-      fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength; universes = universes },
+		fpl initial_goals in
+  let binders =
+    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
+	       universe_binders
+  in
+  { id = pid; entries = entries; persistence = strength;
+    universes = (universes, binders) },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a22545080b..ea7fc7cfa8 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -55,18 +55,18 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Names.Id.t Loc.located list
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
-  (** guards : lemma_possible_guards; *)
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
+		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -80,14 +80,15 @@ 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 :
-  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+  Decl_kinds.goal_kind -> (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  ->
-    proof_terminator -> unit
+  Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+  Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
@@ -140,6 +141,8 @@ val set_used_variables :
   Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+val get_universe_binders : unit -> universe_binders option
+
 (**********************************************************)
 (*                                                        *)
 (*                            Proof modes                 *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6c18326882..5f4e4deb47 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -186,7 +186,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -205,6 +205,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
+    Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
   with e when Errors.noncritical e ->
     let e = Errors.push e in
@@ -219,11 +220,11 @@ let compute_proof_name locality = function
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
         user_err_loc (loc,"",pr_id id ++ str " already exists.");
-      id
+      id, pl
   | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -276,28 +277,28 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs do_guard persistence hook
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  save ?export_seff id const cstrs pl do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
-
 let save_anonymous ?export_seff proof save_ident =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs pl do_guard persistence hook
 
 let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,cstrs,do_guard,_,hook = proof in
+  let id,const,(cstrs,pl),do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs pl do_guard
+      (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
-let admit (id,k,e) hook () =
+let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -306,6 +307,7 @@ let admit (id,k,e) hook () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
+  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -315,11 +317,10 @@ let set_start_hook = (:=) start_hook
 
 
 let get_proof proof do_guard hook opacity =
-  let (id,(const,cstrs,persistence)) =
+  let (id,(const,univs,persistence)) =
     Pfedit.cook_this_proof proof
   in
-  (** FIXME *)
-  id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
+  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
 
 let check_exist =
   List.iter (fun (loc,id) ->
@@ -329,16 +330,16 @@ let check_exist =
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe,ctx) ->
-      admit (id,k,pe) (hook (Some ctx)) ();
+  | Admitted (id,k,pe,(ctx,pl)) ->
+      admit (id,k,pe) pl (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
         | Vernacexpr.Transparent -> false, true, []
         | Vernacexpr.Opaque None -> true, false, []
         | Vernacexpr.Opaque (Some l) -> true, true, l in
-      let proof = get_proof proof compute_guard 
-	(hook (Some proof.Proof_global.universes)) is_opaque in
+      let proof = get_proof proof compute_guard
+	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some ((_,id),None) -> save_anonymous ~export_seff proof id
@@ -350,7 +351,7 @@ let universe_proof_terminator compute_guard hook =
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
-let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id ?pl 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 +359,9 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = universe_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -368,11 +369,11 @@ let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -380,7 +381,7 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
@@ -409,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start")
-  | (id,(t,(_,imps)))::other_thms ->
+  | ((id,pl),(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
         | None -> Evd.empty_evar_universe_context
@@ -428,7 +429,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
@@ -472,14 +473,13 @@ let save_proof ?proof = function
             if const_entry_type = None then
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
-            let ctx = Evd.evar_context_universe_context universes in
+            let ctx = Evd.evar_context_universe_context (fst universes) in
             Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
             let id, k, typ = Pfedit.current_proof_statement () in
             (* This will warn if the proof is complete *)
             let pproofs, universes =
               Proof_global.return_proof ~allow_partial:true () in
-            let ctx = Evd.evar_context_universe_context universes in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
@@ -489,7 +489,10 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
+	    let names = Pfedit.get_universe_binders () in
+            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
+		     (universes, Some binders))
       in
       Proof_global.get_terminator() pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 6556aa2297..376374cb85 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -14,7 +14,6 @@ open Vernacexpr
 open Pfedit
 
 type 'a declaration_hook
-
 val mk_hook :
   (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
 
@@ -24,20 +23,24 @@ 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_map -> ?sign:Environ.named_context_val -> types ->
+val start_proof : Id.t -> ?pl:universe_binders -> 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_map -> ?sign:Environ.named_context_val -> types ->
+val start_proof_univs : Id.t -> ?pl:universe_binders -> 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
+  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  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
+  goal_kind -> Evd.evar_map ->
+  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t * universe_binders option) *
+     (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 val standard_proof_terminator :
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b709a3fc4..91cfddb547 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1128,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -1164,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in