Merge branch 'v8.5'

7 files changed, 106 insertions, 80 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 4122487e23..8ac273c84f 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -304,7 +304,7 @@ let build_beq_scheme mode kn =
 	  raise (NonSingletonProp (kn,i));
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
-       Evd.empty_evar_universe_context (* FIXME *)),
+       Evd.make_evar_universe_context (Global.env ()) None),
       !eff
 
 let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -641,7 +641,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let side_eff = side_effect_of_mode mode in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
@@ -764,12 +764,12 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = Evd.empty_evar_universe_context in
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let side_eff = side_effect_of_mode mode in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx (* FIXME *)), eff
+  ([|ans|], ctx), eff
 
 let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
 
@@ -934,7 +934,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = Evd.empty_evar_universe_context (* FIXME *)in
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 7fe79d948b..805a29e396 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -347,7 +347,7 @@ let named_of_rel_context l =
 
 let context poly l =
   let env = Global.env() in
-  let evars = ref Evd.empty in
+  let evars = ref (Evd.from_env env) in
   let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.map_rel_context subst fullctx in
@@ -358,11 +358,13 @@ let context poly l =
     with e when Errors.noncritical e ->
       error "Anonymous variables not allowed in contexts."
   in
-  let uctx = Evd.universe_context_set !evars in
+  let uctx = ref (Evd.universe_context_set !evars) in
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let uctx = Univ.ContextSet.to_context uctx in	
-      let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in
+      let ctx = Univ.ContextSet.to_context !uctx in
+      (* Declare the universe context once *)
+      let () = uctx := Univ.ContextSet.empty in
+      let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
@@ -379,8 +381,9 @@ let context poly l =
       let impl = List.exists test impls in
       let decl = (Discharge, poly, Definitional) in
       let nstatus =
-        pi3 (Command.declare_assumption false decl (t, uctx) [] impl
+        pi3 (Command.declare_assumption false decl (t, !uctx) [] impl
           Vernacexpr.NoInline (Loc.ghost, id))
       in
-      status && nstatus
+      let () = uctx := Univ.ContextSet.empty in
+	status && nstatus
   in List.fold_left fn true (List.rev ctx)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e2e5d8704e..b65ff73feb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -241,11 +241,14 @@ let interp_assumption evdref env impls bl c =
   let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
 
-let declare_assumptions idl is_coe k c imps impl_is_on nl =
-  let refs, status =
-    List.fold_left (fun (refs,status) id ->
-      let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in
-      (ref',u')::refs, status' && status) ([],true) idl in
+let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl =
+  let refs, status, _ =
+    List.fold_left (fun (refs,status,ctx) id ->
+      let ref',u',status' =
+	declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in
+      (ref',u')::refs, status' && status, Univ.ContextSet.empty)
+      ([],true,ctx) idl
+  in
   List.rev refs, status
 
 let do_assumptions (_, poly, _ as kind) nl l =
@@ -467,16 +470,17 @@ let inductive_levels env evdref poly arities inds =
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
 	in
-	  (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *)
-	  let duu = Sorts.univ_of_sort du in
-	  let evd =
-	    if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
-	      if is_flexible_sort evd duu then
-		Evd.set_eq_sort env evd (Prop Null) du
-	      else evd
-	    else Evd.set_eq_sort env evd (Type cu) du
-	  in
-	    (evd, arity :: arities))
+	let duu = Sorts.univ_of_sort du in
+	let evd =
+	  if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
+	    if is_flexible_sort evd duu then
+	      if Evd.check_leq evd Univ.type0_univ duu then
+	      	evd
+	      else Evd.set_eq_sort env evd (Prop Null) du
+	    else evd
+	  else Evd.set_eq_sort env evd (Type cu) du
+	in
+	  (evd, arity :: arities))
     (!evdref,[]) (Array.to_list levels') destarities sizes
   in evdref := evd; List.rev arities
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 452d5fbe50..ae8ee7670a 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -423,7 +423,7 @@ let fold_left' f = function
 
 let build_combined_scheme env schemes =
   let defs = List.map (fun cst -> (* FIXME *)
-    let evd, c = Evd.fresh_constant_instance env Evd.empty cst in
+    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 find_inductive ty =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0b15ecf33e..d2bd2c07bd 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -625,7 +625,7 @@ let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
   match obl.obl_status with
-  | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) }
+  | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
   | Evar_kinds.Define opaque ->
       let opaque = if get_proofs_transparency () then false else opaque in
       let poly = pi2 prg.prg_kind in
@@ -649,7 +649,7 @@ let declare_obligation prg obl body ty uctx =
       in
 	if not opaque then add_hint false prg constant;
 	definition_message obl.obl_name;
-	{ obl with obl_body = 
+	true, { obl with obl_body =
 	    if poly then 
 	      Some (DefinedObl constant)
 	    else
@@ -798,9 +798,9 @@ let solve_by_tac name evi t poly ctx =
   let entry = Term_typing.handle_entry_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
   assert(Declareops.side_effects_is_empty eff);
-  assert(Univ.ContextSet.is_empty (snd body));
+  let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
-  (fst body), entry.Entries.const_entry_type, ctx'
+  (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx'
 
 let obligation_terminator name num guard hook pf =
   let open Proof_global in
@@ -824,7 +824,7 @@ let obligation_terminator name num guard hook pf =
       let obls, rem = prg.prg_obligations in
       let obl = obls.(num) in
       let ctx = Evd.evar_context_universe_context uctx in
-      let obl = declare_obligation prg obl body ty ctx in
+      let (_, obl) = declare_obligation prg obl body ty ctx in
       let obls = Array.copy obls in
       let _ = obls.(num) <- obl in
       try ignore (update_obls prg obls (pred rem))
@@ -847,9 +847,9 @@ let obligation_hook prg obl num auto ctx' _ gr =
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
-      (* This context is already declared globally, we cannot
-          instantiate the rigid variables anymore *)
-      Evd.abstract_undefined_variables ctx'
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      Evd.evar_universe_context (Evd.from_env (Global.env ()))
     else ctx'
   in
   let prg = { prg with prg_ctx = ctx' } in
@@ -922,8 +922,13 @@ and solve_obligation_by_tac prg obls i tac =
 	        (pi2 !prg.prg_kind) !prg.prg_ctx
 	    in
 	    let uctx = Evd.evar_context_universe_context ctx in
-	      prg := {!prg with prg_ctx = ctx};
-	      obls.(i) <- declare_obligation !prg obl t ty uctx;
+	    let () = prg := {!prg with prg_ctx = ctx} in
+	    let def, obl' = declare_obligation !prg obl t ty uctx in
+	      obls.(i) <- obl';
+	      if def && not (pi2 !prg.prg_kind) then (
+		(* Declare the term constraints with the first obligation only *)
+		let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in
+		  prg := {!prg with prg_ctx = ctx'});
 	      true
 	  else false
 	with e when Errors.noncritical e ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e214f9ca71..60fe76bb82 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,14 +131,21 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
   let evars, nf = Evarutil.nf_evars_and_universes sigma in
   let arity = nf t' in
-  let evars = 
+  let arity, evars = 
     let _, univ = compute_constructor_level evars env_ar newfs in
     let ctx, aritysort = Reduction.dest_arity env0 arity in
       assert(List.is_empty ctx); (* Ensured by above analysis *)
       if Sorts.is_prop aritysort || 
 	(Sorts.is_set aritysort && is_impredicative_set env0) then
-	evars
-      else Evd.set_leq_sort env_ar evars (Type univ) aritysort
+	arity, evars
+      else
+	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
+	  if Univ.is_small_univ univ then
+	    (* We can assume that the level aritysort is not constrained
+  	       and clear it. *)
+	    mkArity (ctx, Sorts.sort_of_univ univ),
+	    Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
+	  else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = map_rel_context nf newps in
@@ -233,7 +240,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let (mib,mip) = Global.lookup_inductive indsp in
   let u = Declareops.inductive_instance mib in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
-  let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in
+  let poly = mib.mind_polymorphic in
+  let ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
@@ -293,7 +301,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes =
+		      if poly then ctx else Univ.UContext.empty;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
@@ -397,44 +406,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
   let impl, projs =
     match fields with
     | [(Name proj_name, _, field)] when def ->
-	let class_body = it_mkLambda_or_LetIn field params in
-        let _class_type = it_mkProd_or_LetIn arity params in
-	let class_entry = 
-	  Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
-	let cst = Declare.declare_constant (snd id)
-	  (DefinitionEntry class_entry, IsDefinition Definition)
-	in
-	let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
-	let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
-	let proj_type =
-	  it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
-	let proj_body =
-	  it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
-	let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
-	let proj_cst = Declare.declare_constant proj_name
-	  (DefinitionEntry proj_entry, IsDefinition Definition)
-	in
-	let cref = ConstRef cst in
-	Impargs.declare_manual_implicits false cref [paramimpls];
-	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
-	Classes.set_typeclass_transparency (EvalConstRef cst) false false;
-	let sub = match List.hd coers with
-	  | Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
-	  | None -> None 
-	in
-	  cref, [Name proj_name, sub, Some proj_cst]
+      let class_body = it_mkLambda_or_LetIn field params in
+      let _class_type = it_mkProd_or_LetIn arity params in
+      let class_entry = 
+	Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
+      let cst = Declare.declare_constant (snd id)
+	(DefinitionEntry class_entry, IsDefinition Definition)
+      in
+      let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+      let inst_type = appvectc (mkConstU cstu)
+			       (Termops.rel_vect 0 (List.length params)) in
+      let proj_type =
+	it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
+      let proj_body =
+	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
+      let proj_entry =
+	Declare.definition_entry ~types:proj_type ~poly
+	    ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
+      in
+      let proj_cst = Declare.declare_constant proj_name
+        (DefinitionEntry proj_entry, IsDefinition Definition)
+      in
+      let cref = ConstRef cst in
+      Impargs.declare_manual_implicits false cref [paramimpls];
+      Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+      Classes.set_typeclass_transparency (EvalConstRef cst) false false;
+      let sub = match List.hd coers with
+	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
+	| None -> None 
+      in
+      cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
-	in
-	let coers = List.map2 (fun coe pri -> 
-			       Option.map (fun b -> 
-			         if b then Backward, pri else Forward, pri) coe) 
+       in
+       let coers = List.map2 (fun coe pri -> 
+			      Option.map (fun b -> 
+			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
-	in
-	  IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
-			 (List.rev fields) coers (Recordops.lookup_projections ind))
+       in
+       let l = List.map3 (fun (id, _, _) b y -> (id, b, y))
+         (List.rev fields) coers (Recordops.lookup_projections ind)
+       in IndRef ind, l
   in
   let ctx_context =
     List.map (fun (na, b, t) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ae6ac2bc3..c07c756c01 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -76,9 +76,8 @@ let show_universes () =
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
-  let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in
     msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
-    msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs)
+    msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
@@ -1185,8 +1184,9 @@ let default_env () = {
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let env = Global.env() in
-    let t,ctx = Constrintern.interp_type env Evd.empty c in
-    let t = Detyping.detype false [] env Evd.empty t in
+    let sigma = Evd.from_env env in
+    let t,ctx = Constrintern.interp_type env sigma c in
+    let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in
     let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl