Merge ../../coq/git into trunk

kernel/cooking.ml

@@ -163,10 +163,6 @@ let cook_constant env r =
   let typ = 
     abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps 
   in
-  let univs = 
-    if cb.const_polymorphic then
-      Context.union abs_ctx cb.const_universes
-    else cb.const_universes
-  in
+  let univs = Context.union abs_ctx cb.const_universes in
   (body, typ, cb.const_polymorphic, univs, cb.const_inline_code, 
    Some const_hyps)

kernel/inductive.ml

@@ -61,6 +61,11 @@ let inductive_instance mib =
     Context.instance mib.mind_universes
   else Instance.empty
 
+let inductive_context mib =
+  if mib.mind_polymorphic then 
+    mib.mind_universes 
+  else Univ.Context.empty
+
 let instantiate_inductive_constraints mib subst =
   if mib.mind_polymorphic then
     instantiate_univ_context subst mib.mind_universes
@@ -97,10 +102,12 @@ let instantiate_params full t args sign =
   let () = if not (List.is_empty rem_args) then fail () in
   substl subs ty
 
-let full_inductive_instantiate mib params sign =
+let full_inductive_instantiate mib u params sign =
   let dummy = prop_sort in
   let t = mkArity (sign,dummy) in
-  fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
+  let subst = make_inductive_subst mib u in
+  let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
+    Sign.subst_univs_context subst ar
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
   let subst = make_inductive_subst mib u in
@@ -256,9 +263,9 @@ let inductive_sort_family mip =
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
 
-let get_instantiated_arity (mib,mip) params =
+let get_instantiated_arity (ind,u) (mib,mip) params =
   let sign, s = mind_arity mip in
-  full_inductive_instantiate mib params sign, s
+  full_inductive_instantiate mib u params sign, s
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
@@ -289,7 +296,7 @@ let check_allowed_sort ksort specif =
     raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
 let is_correct_arity env c pj ind specif params =
-  let arsign,_ = get_instantiated_arity specif params in
+  let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar u =
     let pt' = whd_betadeltaiota env pt in
     match kind_of_term pt', ar with

kernel/inductive.mli

@@ -37,6 +37,7 @@ val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -
 val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_subst
 
 val inductive_instance : mutual_inductive_body -> universe_instance
+val inductive_context : mutual_inductive_body -> universe_context
 
 val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints
 

library/declare.ml

@@ -50,37 +50,39 @@ let add_cache_hook f = cache_hook := f
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of (constr * types option) Univ.in_universe_context_set * bool (** opacity *)
-  | SectionLocalAssum of types Univ.in_universe_context_set * bool (** Implicit status *)
+  | SectionLocalDef of (constr * types option) Univ.in_universe_context_set * polymorphic * bool (** opacity *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
-  | Inl cst -> Global.add_constraints cst
+  | Inl ctx -> Global.push_context_set ctx
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
     alreadydeclared (pr_id id ++ str " already exists");
-  let impl,opaq,ctx,cst = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx), impl) ->
-        let cst = Global.push_named_assum (id,ty) in
+  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ((ty,ctx),poly,impl) ->
+        let _cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Implicit else Explicit in
-	impl, true, ctx, cst
-    | SectionLocalDef (((c,t),ctx),opaq) ->
-        let cst = Global.push_named_def (id,c,t) in
-        Explicit, opaq, ctx, cst in
+	impl, true, poly, ctx
+    | SectionLocalDef (((c,t),ctx),poly,opaq) ->
+        let _cst = Global.push_named_def (id,c,t) in
+        Explicit, opaq, poly, ctx in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl ctx;
+  add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
-  add_variable_data id (p,opaq,ctx,cst,mk)
+  add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> Some (Inl (variable_constraints id))
+  | Inr (id,_) -> 
+    if variable_polymorphic id then None
+    else Some (Inl (variable_context id))
   | Inl _ -> Some o
 
 type variable_obj =
-    (Univ.constraints, Id.t * variable_declaration) union
+    (Univ.ContextSet.t, Id.t * variable_declaration) union
 
 let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
@@ -141,7 +143,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
+  add_section_constant kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind;
   !cache_hook sp
@@ -267,7 +269,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
+  add_section_kn kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
   List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)

library/declare.mli

@@ -29,8 +29,8 @@ open Nametab
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of (constr * types option) Univ.in_universe_context_set * bool (** opacity *)
-  | SectionLocalAssum of types Univ.in_universe_context_set * bool (** Implicit status *)
+  | SectionLocalDef of (constr * types option) Univ.in_universe_context_set * polymorphic * bool (** opacity *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 

library/decls.ml

@@ -18,7 +18,7 @@ open Libnames
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.universe_context_set * Univ.constraints * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind
 
 let vartab = ref (Id.Map.empty : variable_data Id.Map.t)
 
@@ -33,7 +33,7 @@ let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p
 let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq
 let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k
 let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx
-let variable_constraints id = let (_,_,_,cst,_) = Id.Map.find id !vartab in cst
+let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in

library/decls.mli

@@ -18,15 +18,15 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (** opacity *) * Univ.universe_context_set * Univ.constraints * logical_kind
+  DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_context : variable -> Univ.universe_context_set
-val variable_constraints : variable -> Univ.constraints
+val variable_polymorphic : variable -> polymorphic
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)

library/lib.ml

@@ -408,21 +408,22 @@ type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t *
   variable_context Univ.in_universe_context Names.Mindmap.t
 
 let sectab =
-  ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * Univ.universe_context_set) list *
+  ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
+		Decl_kinds.polymorphic * Univ.universe_context_set) list *
 		Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
-let add_section_variable id impl ctx =
+let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,ctx)::vars,repl,abs)::sl
+	sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
 
-let extract_hyps poly (secs,ohyps) =
+let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+    | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
     | (id::idl,hyps) -> aux (idl,hyps)
@@ -438,22 +439,22 @@ let instance_from_variable_context sign =
 
 let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
 
-let add_section_replacement f g poly hyps =
+let add_section_replacement f g hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
-    let sechyps,ctx = extract_hyps poly (vars,hyps) in
+    let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
     sectab := (vars,f (Univ.Context.instance ctx,args) exps,g (sechyps,ctx) abs)::sl
 
-let add_section_kn poly kn =
+let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-  add_section_replacement f f poly
+  add_section_replacement f f
 
-let add_section_constant poly kn =
+let add_section_constant kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-  add_section_replacement f f poly
+  add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
 
@@ -469,7 +470,8 @@ let rec list_mem_assoc x = function
 
 let section_instance = function
   | VarRef id ->
-      if List.exists (fun (id',_,_) -> Names.id_eq id id') (pi1 (List.hd !sectab)) 
+      if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
+	(pi1 (List.hd !sectab))
       then Univ.Instance.empty, [||]
       else raise Not_found
   | ConstRef con ->

library/lib.mli

@@ -193,10 +193,10 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Univ.universe_context_set -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
 
-val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Sign.named_context -> unit
-val add_section_kn : Decl_kinds.polymorphic -> Names.mutual_inductive -> Sign.named_context -> unit
+val add_section_constant : Names.constant -> Sign.named_context -> unit
+val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit -> Cooking.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)

plugins/funind/indfun_common.ml

@@ -157,7 +157,7 @@ let save with_clean id const (locality,p,kind) hook =
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
 	let ctx = Univ.ContextSet.of_context univs in
-	let c = SectionLocalDef (((pft, tpo), ctx), opacity) in
+	let c = SectionLocalDef (((pft, tpo), ctx), p, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Discharge | Local | Global ->

pretyping/inductiveops.ml

@@ -262,6 +262,7 @@ let instantiate_context sign args =
 
 let get_arity env ((ind,u),params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let univsubst = make_inductive_subst mib u in
   let parsign =
     (* Dynamically detect if called with an instance of recursively
        uniform parameter only or also of non recursively uniform
@@ -272,9 +273,11 @@ let get_arity env ((ind,u),params) =
       snd (List.chop nnonrecparams mib.mind_params_ctxt)
     else
       parsign in
+  let parsign = Sign.subst_univs_context univsubst parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
   let subst = instantiate_context parsign params in
+  let arsign = Sign.subst_univs_context univsubst arsign in
   (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
 (* Functions to build standard types related to inductive *)

tactics/elimschemes.ml

@@ -56,12 +56,13 @@ let optimize_non_type_induction_scheme kind dep sort ind =
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
-  let u = 
+  let ctx = 
     let mib,mip = Inductive.lookup_mind_specif env ind in
-      Inductive.inductive_instance mib
+      Inductive.inductive_context mib
   in
-  let ctx = Univ.ContextSet.of_instance u in
-  let sigma, c = build_induction_scheme env (Evd.from_env ~ctx env) (ind,u) dep sort in
+  let u = Univ.Context.instance ctx in
+  let ctxset = Univ.ContextSet.of_context ctx in
+  let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ctxset env) (ind,u) dep sort in
     c, Evd.evar_universe_context sigma
 
 let rect_scheme_kind_from_type =

toplevel/classes.ml

@@ -370,7 +370,7 @@ let context l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let decl = (Discharge, true, Definitional) in
+      let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in
       let nstatus =
         Command.declare_assumption false decl (t, uctx) [] impl
           Vernacexpr.NoInline (Loc.ghost, id)

toplevel/command.ml

@@ -155,7 +155,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     let c =
       let bt = (ce.const_entry_body, ce.const_entry_type) in
       let ctx = Univ.ContextSet.of_context ce.const_entry_universes in
-        SectionLocalDef((bt,ctx),false) in
+        SectionLocalDef((bt,ctx),p,false) in
     let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
     let () = definition_message ident in
     let () = if Pfedit.refining () then
@@ -193,7 +193,7 @@ let do_definition ident k bl red_option c ctypopt hook =
 
 let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with
 | Discharge when Lib.sections_are_opened () ->
-  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),impl), IsAssumption kind) in
+  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let () =

toplevel/discharge.ml

@@ -83,11 +83,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let univs = 
-    if mib.mind_polymorphic then
-      Univ.Context.union abs_ctx mib.mind_universes
-    else mib.mind_universes
-  in
+  let univs = Univ.Context.union abs_ctx mib.mind_universes in
   { mind_entry_record = mib.mind_record;
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params';

toplevel/lemmas.ml

@@ -169,7 +169,7 @@ let save id const do_guard (locality,poly,kind) hook =
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let ctx = Univ.ContextSet.of_context univs in
-	let c = SectionLocalDef (((pft, tpo), ctx), opacity) in
+	let c = SectionLocalDef (((pft, tpo), ctx), poly, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Local | Global | Discharge ->
@@ -204,7 +204,7 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx_i),impl) in
+          let c = SectionLocalAssum ((t_i,ctx_i),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
       | Local | Global ->
@@ -226,7 +226,7 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
         | _ -> anomaly (Pp.str "Not a proof by induction") in
       match locality with
       | Discharge ->
-	  let c = SectionLocalDef (((body_i, Some t_i), ctx_i), opaq) in
+	  let c = SectionLocalDef (((body_i, Some t_i), ctx_i), p, opaq) in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
       | Local | Global ->