diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 17:11:12 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 17:11:36 +0200 |
commit | 30a908becf31d91592a1f7934cfa3df2d67d1834 (patch) | |
tree | 264176851bd7f316a5425f84aeccaac952793440 | |
parent | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (diff) |
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
41 files changed, 232 insertions, 363 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 637744df3..328ddd0cd 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -546,8 +546,7 @@ let rec tmpp v loc = | DefineBody (_, None , ce, None) -> ce | DefineBody (_, Some _, ce, Some _) -> ce | DefineBody (_, None , ce, Some _) -> ce in - let def_kind = { locality = l; polymorphic = false; object_kind = dk } in - let str_dk = Kindops.string_of_definition_kind def_kind in + let str_dk = Kindops.string_of_definition_kind (l, false, dk) in let str_id = Id.to_string id in (xmlDef str_dk str_id loc [pp_expr e]) | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 2644a56b3..59c24900d 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -17,7 +17,7 @@ open Decl_kinds (***********************) (* For binders parsing *) -let implicit_status_eq bk1 bk2 = match bk1, bk2 with +let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true | Implicit, Implicit -> true | _ -> false @@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with | _ -> false let binder_kind_eq b1 b2 = match b1, b2 with -| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2 +| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 && + binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false @@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 = | CPrim(_,i1), CPrim(_,i2) -> prim_token_eq i1 i2 | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) -> - implicit_status_eq bk1 bk2 && + binding_kind_eq bk1 bk2 && Option.equal abstraction_kind_eq ak1 ak2 && constr_expr_eq e1 e2 | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index bfe546ba5..a92da035f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool val local_binder_eq : local_binder -> local_binder -> bool (** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) -val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool -(** Equality on [implicit_status] *) +val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool +(** Equality on [binding_kind] *) val binder_kind_eq : binder_kind -> binder_kind -> bool (** Equality on [binder_kind] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 62cb62f49..f7fcbb4ee 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with | Name id, CProdN (loc,[nal,Default bk',ty],c) - when implicit_status_eq bk bk' && constr_expr_eq aty ty + when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> @@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with | CLambdaN (loc,[nal,Default bk',ty],c) - when implicit_status_eq bk bk' && constr_expr_eq aty ty + when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 863f33b18..0e5602078 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -65,7 +65,7 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) type ltac_sign = { ltac_vars : Id.Set.t; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 718aa753e..eea76aa31 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -75,7 +75,7 @@ type ltac_sign = { val empty_ltac_sign : ltac_sign -type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c65d43db3..6b29b6d3d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 @@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in - let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in + let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t') + alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t') + alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> let alp, p = unify_pat alp p p' in - alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t') + alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -1122,7 +1122,7 @@ let term_of_binder = function | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.implicit_status * + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * glob_constr option * glob_constr let match_notation_constr u c (metas,pat) = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 6428ccab6..854e222e3 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr exception No_match type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.implicit_status * + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index e494b2f81..0cbb29575 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -23,8 +23,8 @@ type explicitation = | ExplByName of Id.t type binder_kind = - | Default of implicit_status - | Generalized of implicit_status * implicit_status * bool + | Default of binding_kind + | Generalized of binding_kind * binding_kind * bool (** Inner binding, outer bindings, typeclass-specific flag for implicit generalization of superclasses *) @@ -95,7 +95,7 @@ and constr_expr = | CSort of Loc.t * glob_sort | CCast of Loc.t * constr_expr * constr_expr cast_type | CNotation of Loc.t * notation * constr_notation_substitution - | CGeneralization of Loc.t * implicit_status * abstraction_kind option * constr_expr + | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr @@ -132,7 +132,7 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder list list (** for binders subexpressions *) -type typeclass_constraint = (Name.t located * Id.t located list option) * implicit_status * constr_expr +type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index c117baf3f..6a4e18833 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -10,10 +10,7 @@ type locality = Discharge | Local | Global -type implicit_status = Explicit | Implicit - -type binding_kind = implicit_status -(** @deprecated Alias type *) +type binding_kind = Explicit | Implicit type polymorphic = bool @@ -52,13 +49,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type 'a declaration_kind = { locality : locality; - polymorphic : bool; - object_kind : 'a } - -type assumption_kind = assumption_object_kind declaration_kind +type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = definition_object_kind declaration_kind +type definition_kind = locality * polymorphic * definition_object_kind (** Kinds used in proofs *) @@ -66,7 +59,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = goal_object_kind declaration_kind +type goal_kind = locality * polymorphic * goal_object_kind (** Kinds used in library *) diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 178952fef..b3159c860 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -40,8 +40,8 @@ type glob_constr = | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list - | GLambda of Loc.t * Name.t * implicit_status * glob_constr * glob_constr - | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr + | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) @@ -54,7 +54,7 @@ type glob_constr = | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option) | GCast of Loc.t * glob_constr * glob_constr cast_type -and glob_decl = Name.t * implicit_status * glob_constr option * glob_constr +and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr and fix_recursion_order = | GStructRec diff --git a/library/declare.ml b/library/declare.ml index 5c6543e28..cc8415cf4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,9 +44,7 @@ let if_xml f x = if !Flags.xml_export then f x else () type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; - polymorphic : bool; - implicit_status : implicit_status } + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -58,22 +56,19 @@ let cache_variable ((sp,_),o) = if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum { type_context = (ty,ctx); polymorphic; implicit_status } -> - let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in - implicit_status, true, polymorphic, ctx + let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum ((ty,ctx),poly,impl) -> + let () = Global.push_named_assum ((id,ty,poly),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl ~polymorphic ctx; + add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id { dir_path = p; - opaque; - universe_context_set = ctx; - polymorphic; - kind = mk } + add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with | Inr (id,_) -> @@ -241,11 +236,11 @@ let declare_constant_common id cst = c let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(polymorphic=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; - const_entry_polymorphic = polymorphic; + const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; @@ -277,9 +272,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(polymorphic=false) id ?types (body,ctx) = + ?(poly=false) id ?types (body,ctx) = let cb = - definition_entry ?types ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -463,10 +458,10 @@ let input_universes : universe_decl -> Libobject.obj = discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); classify_function = (fun a -> Keep a) } -let do_universe ~polymorphic l = +let do_universe poly l = let in_section = Lib.sections_are_opened () in let () = - if polymorphic && not in_section then + if poly && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in @@ -475,7 +470,7 @@ let do_universe ~polymorphic l = let lev = Universes.new_univ_level (Global.current_dirpath ()) in (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (polymorphic, l)) + Lib.add_anonymous_leaf (input_universes (poly, l)) type constraint_decl = polymorphic * Univ.constraints @@ -495,7 +490,7 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint ~polymorphic l = +let do_constraint poly l = let u_of_id = let names, _ = Universes.global_universe_names () in fun (loc, id) -> @@ -505,12 +500,12 @@ let do_constraint ~polymorphic l = in let in_section = Lib.sections_are_opened () in let () = - if polymorphic && not in_section then + if poly && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = - if polymorphic then () + if poly then () else if p || p' then let loc = if p then loc else loc' in user_err ~loc ~hdr:"Constraint" @@ -524,4 +519,4 @@ let do_constraint ~polymorphic l = Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (polymorphic, constraints)) + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index a0ec26444..7824506da 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,9 +23,7 @@ open Decl_kinds type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; - polymorphic : bool; - implicit_status : implicit_status } + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -44,7 +42,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?polymorphic:bool -> ?univs:Univ.universe_context -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -58,7 +56,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?polymorphic:bool -> Id.t -> ?types:constr -> + ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant (** Since transparent constants' side effects are globally declared, we @@ -91,6 +89,5 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -val do_universe : polymorphic:bool -> Id.t Loc.located list -> unit -val do_constraint : polymorphic:bool -> - (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/decls.ml b/library/decls.ml index 1e9afe968..2952c258a 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,22 +19,18 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - { dir_path : DirPath.t; - opaque : bool; - universe_context_set : Univ.universe_context_set; - polymorphic : bool; - kind : logical_kind } + DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = (Id.Map.find id !vartab).dir_path -let variable_opacity id = (Id.Map.find id !vartab).opaque -let variable_kind id = (Id.Map.find id !vartab).kind -let variable_context id = (Id.Map.find id !vartab).universe_context_set -let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic +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_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 diff --git a/library/decls.mli b/library/decls.mli index e84a6376b..1ca7f8946 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -17,11 +17,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - { dir_path : DirPath.t; - opaque : bool; - universe_context_set : Univ.universe_context_set; - polymorphic : bool; - kind : 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 diff --git a/library/kindops.ml b/library/kindops.ml index 3d737e5ac..21b1bec33 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,9 +24,9 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - let locality = def.locality in + let (locality, poly, kind) = def in let error () = CErrors.anomaly (Pp.str "Internal definition kind") in - match def.object_kind with + match kind with | Definition -> begin match locality with | Discharge -> "Let" diff --git a/library/lib.ml b/library/lib.ml index 13921610d..749cc4ff3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -391,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.implicit_status * + | Variable of (Names.Id.t * Decl_kinds.binding_kind * Decl_kinds.polymorphic * Univ.universe_context_set) | Context of Univ.universe_context_set @@ -416,12 +416,12 @@ let check_same_poly p vars = if List.exists pred vars then error "Cannot mix universe polymorphic and monomorphic declarations in sections." -let add_section_variable id impl ~polymorphic ctx = +let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; - sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -450,11 +450,11 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst -let add_section_replacement f g ~polymorphic hyps = +let add_section_replacement f g poly hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly polymorphic vars in + let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -462,13 +462,13 @@ let add_section_replacement f g ~polymorphic hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn ~polymorphic kn = +let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f ~polymorphic + add_section_replacement f f poly -let add_section_constant ~polymorphic kn = +let add_section_constant poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f ~polymorphic + add_section_replacement f f poly let replacement_context () = pi2 (List.hd !sectab) diff --git a/library/lib.mli b/library/lib.mli index 51c74d395..092643c2d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,7 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -176,11 +176,11 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab 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.implicit_status -> polymorphic:bool -> 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_context : Univ.universe_context_set -> unit -val add_section_constant : polymorphic:bool -> +val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Context.Named.t -> unit -val add_section_kn : polymorphic:bool -> +val add_section_kn : Decl_kinds.polymorphic -> Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index ef9d49998..a332e2871 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1755,7 +1755,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance ~polymorphic:(Flags.is_universe_polymorphism ()) + new_instance (Flags.is_universe_polymorphism ()) binders instance (Some (true, CRecord (Loc.ghost,fields))) ~global ~generalize:false ~refine:false None @@ -1828,7 +1828,7 @@ let proper_projection r ty = it_mkLambda_or_LetIn app ctx let declare_projection n instance_id r = - let polymorphic = Global.is_polymorphic r in + let poly = Global.is_polymorphic r in let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in @@ -1858,7 +1858,7 @@ let declare_projection n instance_id r = let typ = it_mkProd_or_LetIn typ ctx in let pl, ctx = Evd.universe_context sigma in let cst = - Declare.definition_entry ~types:typ ~polymorphic ~univs:ctx term + Declare.definition_entry ~types:typ ~poly ~univs:ctx term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1942,9 +1942,8 @@ let add_morphism_infer glob m n = poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else - let kind = { locality = Decl_kinds.Global; - polymorphic = poly; - object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance } + let kind = Decl_kinds.Global, poly, + Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ = function @@ -1963,7 +1962,7 @@ let add_morphism_infer glob m n = let add_morphism glob binders m s n = init_setoid (); - let polymorphic = Flags.is_universe_polymorphism () in + let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = (((Loc.ghost,Name instance_id),None), Explicit, @@ -1972,7 +1971,7 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob ~polymorphic binders instance + ignore(new_instance ~global:glob poly binders instance (Some (true, CRecord (Loc.ghost,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 12fd8359a..e39d17b52 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,10 +22,7 @@ let start_deriving f suchthat lemma = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.{ locality = Global; - polymorphic = false; - object_kind = DefinitionBody Definition } - in + let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in (** create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bba7b3c59..527f4f0b1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -996,9 +996,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - Decl_kinds.{ locality = Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Proof Theorem } + (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 4f5f167c2..cc699e5d3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -288,9 +288,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd new_principle_type hook @@ -341,9 +339,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~polymorphic:(Flags.is_universe_polymorphism ()) - ~univs:(snd (Evd.universe_context evd')) value - in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbc1507f..99b04898b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -395,9 +395,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname - { locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Definition } pl + (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8c6673732..a45effb16 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -148,18 +148,17 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const goal_kind hook = +let save with_clean id const (locality,_,kind) hook = let fix_exn = Future.fix_exn_of const.const_entry_body in - let locality = goal_kind.locality in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> - let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) | Discharge | Local | Global -> let local = get_locality locality in - let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6d042b3a4..c8b4e4833 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -832,9 +832,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) !evd typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -895,13 +893,10 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - Lemmas.start_proof lem_id - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } - sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + Lemmas.start_proof lem_id + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (fst lemmas_types_infos.(i)) + (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 75495ed98..f43251bc5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1348,9 +1348,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in Lemmas.start_proof na - { locality = Decl_kinds.Global; - polymorphic = false (* FIXME *); - object_kind = Decl_kinds.Proof Decl_kinds.Lemma } + (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () @@ -1396,12 +1394,8 @@ let com_terminate hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in - let goal_kind = { locality = Global; - polymorphic = false; (* FIXME *) - object_kind = Proof Lemma } - in Lemmas.start_proof thm_name - goal_kind ~sign:(Environ.named_context_val env) + (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (compute_terminate_type nb_args fonctional_ref) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); @@ -1451,11 +1445,7 @@ let (com_eqn : int -> Id.t -> let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let goal_kind = { locality = Global; - polymorphic = false; - object_kind = Proof Lemma } - in - (Lemmas.start_proof eq_name goal_kind + (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evmap equation_lemma_type diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9a8ad00d0..51fc289b4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -695,8 +695,7 @@ module Make | VernacDefinition (d,id,b) -> (* A verifier... *) let pr_def_token (l,dk) = let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind - { locality = l; polymorphic = false; object_kind = dk }) + keyword (Kindops.string_of_definition_kind (l,false,dk)) in let pr_reduce = function | None -> mt() diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d55d6ce6b..86c2b7a57 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -147,10 +147,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let default_goal_kind = - { locality = Global; polymorphic = false; object_kind = Proof Theorem } - -let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac = +let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in start_proof id goal_kind evd sign typ terminator; @@ -164,10 +161,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ ta delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac = +let build_by_tactic ?(side_eff=true) 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 = { locality = Global; polymorphic; object_kind = Proof Theorem } in + let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index aa01969b7..f2f4b11ed 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -169,7 +169,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 911d4ffbc..2956d623f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -320,7 +320,7 @@ let constrain_variables init uctx = let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in - let poly = strength.Decl_kinds.polymorphic in + let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in @@ -398,7 +398,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = - let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in + let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in diff --git a/stm/lemmas.ml b/stm/lemmas.ml index b1b8aa288..2ab3b9c59 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -191,12 +191,11 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save ?export_seff id const cstrs pl do_guard - { locality; polymorphic; object_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 - let k = Kindops.logical_kind_of_goal_kind object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in @@ -230,20 +229,16 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None -let save_remaining_recthms { locality; polymorphic; object_kind } - norm ctx body opaq i ((id,pl),(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 -> (match locality with | Discharge -> - let impl = Explicit in (* copy values from Vernacentries *) + let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum { type_context = (t_i,ctx); - polymorphic; - implicit_status = impl } - in - let _ = declare_variable id (Lib.cwd(),c,k) in + let c = SectionLocalAssum ((t_i,ctx),p,impl) in + let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> let k = IsAssumption Conjectural in @@ -253,12 +248,12 @@ let save_remaining_recthms { locality; polymorphic; object_kind } | Discharge -> assert false in let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,polymorphic,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> let body = norm body in - let k = Kindops.logical_kind_of_goal_kind object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let rec body_i t = match kind_of_term t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) @@ -269,7 +264,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind } let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~polymorphic + let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p ~univs:(Univ.ContextSet.to_context ctx) body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in @@ -282,7 +277,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind } | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~polymorphic ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -308,10 +303,7 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) save ?export_seff save_ident const cstrs pl do_guard - { locality = Global; - polymorphic = const.const_entry_polymorphic; - object_kind = Proof kind} - hook + (Global, const.const_entry_polymorphic, Proof kind) hook (* Admitted *) @@ -322,9 +314,9 @@ let warn_let_as_axiom = let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in - let () = match k.locality with - | Global -> () - | Local | Discharge -> warn_let_as_axiom id + let () = match k with + | Global, _, _ -> () + | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; @@ -471,7 +463,7 @@ let start_proof_com kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in - (compute_proof_name kind.locality sopt, + (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) @@ -485,7 +477,7 @@ let start_proof_com kind thms hook = | Some l -> ignore (Evd.universe_context evd ?names:l) in let evd = - if kind.polymorphic then evd + if pi2 kind then evd else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in @@ -520,7 +512,7 @@ let save_proof ?proof = function let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, k.polymorphic, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in @@ -541,7 +533,7 @@ let save_proof ?proof = function let names = Pfedit.get_universe_binders () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.universe_context ?names evd in - Admitted(id,k,(sec_vars, k.polymorphic, (typ, ctx), None), + Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c7b8e6cc0..d80e86241 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ()) + let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 86c0b9dd5..9d0e9f084 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4888,9 +4888,7 @@ let anon_id = Id.of_string "anonymous" let tclABSTRACT name_op tac = let open Proof_global in - let default_gk = - { locality = Global; polymorphic = false; object_kind = Proof Theorem } - in + let default_gk = (Global, false, Proof Theorem) in let s, gk = match name_op with | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk diff --git a/toplevel/class.ml b/toplevel/class.ml index 9582015a0..0dc799014 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -180,7 +180,7 @@ let error_not_transparent source = user_err ~hdr:"build_id_coercion" (pr_class source ++ str " must be a transparent constant.") -let build_id_coercion idf_opt source ~polymorphic = +let build_id_coercion idf_opt source poly = let env = Global.env () in let sigma = Evd.from_env env in let sigma, vs = match source with @@ -221,7 +221,7 @@ let build_id_coercion idf_opt source ~polymorphic = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~polymorphic ~univs:(snd (Evd.universe_context sigma)) + (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index a0a8d2aaf..ad4a13c21 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -106,7 +106,7 @@ let instance_hook k pri global imps ?hook cst = Typeclasses.declare_instance pri (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k pri global imps ?hook id pl ~polymorphic evm term termtype = +let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype = let kind = IsDefinition Instance in let evm = let levels = Univ.LSet.union (Universes.universes_of_constr termtype) @@ -115,7 +115,7 @@ let declare_instance_constant k pri global imps ?hook id pl ~polymorphic evm ter in let pl, uctx = Evd.universe_context ?names:pl evm in let entry = - Declare.definition_entry ~types:termtype ~polymorphic ~univs:uctx term + Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -124,7 +124,7 @@ let declare_instance_constant k pri global imps ?hook id pl ~polymorphic evm ter instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~polymorphic ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -197,7 +197,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ let pl, ctx = Evd.universe_context ?names:pl !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry - (None,polymorphic,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Universes.register_universe_binders (ConstRef cst) pl; instance_hook k pri global imps ?hook (ConstRef cst); id @@ -294,12 +294,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id pl - ~polymorphic evm (Option.get term) termtype + poly evm (Option.get term) termtype else if Flags.is_program_mode () || refine || Option.is_empty term then begin - let kind = { locality = Decl_kinds.Global; - polymorphic; - object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance } - in + let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if Flags.is_program_mode () then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in @@ -316,12 +313,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ in let hook = Lemmas.mk_hook hook in let ctx = Evd.evar_universe_context evm in - let kind = { locality = Global; - polymorphic; - object_kind = Instance } - in - ignore (Obligations.add_definition id ?term:constr - ?pl typ ctx ~kind ~hook obls); + ignore (Obligations.add_definition id ?term:constr + ?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls); id else (Flags.silently @@ -397,11 +390,8 @@ let context poly l = | ExplByPos (_, Some id') -> Id.equal id id' | _ -> false in - let impl = if List.exists test impls then Implicit else Explicit in - let decl = { locality = Discharge; - polymorphic = poly; - object_kind = Definitional } - in + let impl = List.exists test impls in + let decl = (Discharge, poly, Definitional) in let nstatus = pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index fc7371cf7..7beb873e6 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -31,7 +31,7 @@ val declare_instance_constant : ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) Id.t Loc.located list option -> - polymorphic:bool -> + bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) @@ -41,7 +41,7 @@ val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) - polymorphic:bool -> + Decl_kinds.polymorphic -> local_binder list -> typeclass_constraint -> (bool * constr_expr) option -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 7bb016d34..caa20b534 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -90,7 +90,7 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl ~polymorphic red_option c ctypopt = +let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in @@ -109,7 +109,7 @@ let interp_definition pl bl ~polymorphic red_option c ctypopt = let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, - definition_entry ~univs:uctx ~polymorphic body + definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -133,7 +133,7 @@ let interp_definition pl bl ~polymorphic red_option c ctypopt = let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, - definition_entry ~types:typ ~polymorphic + definition_entry ~types:typ ~poly:p ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps @@ -174,8 +174,7 @@ let warn_definition_not_visible = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals") -let declare_definition ident def_kind ce pl imps hook = - let { locality = local; object_kind = k; _ } = def_kind in +let declare_definition ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with @@ -198,7 +197,7 @@ let _ = Obligations.declare_definition_ref := let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = - interp_definition pl bl k.polymorphic red_option c ctypopt + interp_definition pl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in @@ -224,48 +223,43 @@ let do_definition ident k pl bl red_option c ctypopt hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) = - let { locality = local; polymorphic; object_kind = kind } = assumption_kind in - match local with - | Discharge when Lib.sections_are_opened () -> - let entry = SectionLocalAssum { type_context = (c,ctx); - polymorphic; - implicit_status = impl } - in - let decl = (Lib.cwd(), entry, IsAssumption kind) in - let _ = declare_variable ident decl in - let () = assumption_message ident in - let () = - if is_verbose () && Pfedit.refining () then - Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ - strbrk " is not visible from current goals") - in - let r = VarRef ident in - let () = Typeclasses.declare_instance None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true false in - (r,Univ.Instance.empty,true) - - | Global | Local | Discharge -> - let local = get_locality ident local in - let inl = match nl with - | NoInline -> None - | DefaultInline -> Some (Flags.get_inline_level()) - | InlineAt i -> Some i - in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,polymorphic,(c,ctx),inl), IsAssumption kind) in - let kn = declare_constant ident ~local decl in - let gr = ConstRef kn in - let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in - let () = assumption_message ident in - let () = Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr ~local polymorphic in - let inst = - if polymorphic then Univ.UContext.instance ctx - else Univ.Instance.empty - in - (gr,inst,Lib.is_modtype_strict ()) +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = +match local with +| Discharge when Lib.sections_are_opened () -> + let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in + let _ = declare_variable ident decl in + let () = assumption_message ident in + let () = + if is_verbose () && Pfedit.refining () then + Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ + strbrk " is not visible from current goals") + in + let r = VarRef ident in + let () = Typeclasses.declare_instance None true r in + let () = if is_coe then Class.try_add_new_coercion r ~local:true false in + (r,Univ.Instance.empty,true) + +| Global | Local | Discharge -> + let local = get_locality ident local in + let inl = match nl with + | NoInline -> None + | DefaultInline -> Some (Flags.get_inline_level()) + | InlineAt i -> Some i + in + let ctx = Univ.ContextSet.to_context ctx in + let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in + let kn = declare_constant ident ~local decl in + let gr = ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in + let () = assumption_message ident in + let () = Typeclasses.declare_instance None false gr in + let () = if is_coe then Class.try_add_new_coercion gr local p in + let inst = + if p (* polymorphic *) then Univ.UContext.instance ctx + else Univ.Instance.empty + in + (gr,inst,Lib.is_modtype_strict ()) let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in @@ -284,12 +278,12 @@ let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = in List.rev refs, status -let do_assumptions_unbound_univs kind nl l = +let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let open Context.Named.Declaration in let env = Global.env () in let evdref = ref (Evd.from_env env) in let l = - if kind.polymorphic then + if poly then (* Separate declarations so that A B : Type puts A and B in different levels. *) List.fold_right (fun (is_coe,(idl,c)) acc -> List.fold_right (fun id acc -> @@ -311,7 +305,7 @@ let do_assumptions_unbound_univs kind nl l = let l = List.map (on_pi2 (nf_evar evd)) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps Explicit nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs @@ -329,13 +323,13 @@ let do_assumptions_bound_univs coe kind nl id pl c = let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls Explicit nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in st let do_assumptions kind nl l = match l with | [coe, ([id, Some pl], c)] -> - let () = match kind.locality with - | Discharge when Lib.sections_are_opened () -> + let () = match kind with + | (Discharge, _, _) when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ~loc msg @@ -858,11 +852,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) kind pl ctx f ((def,_),eff) t imps = - let polymorphic = kind.polymorphic in - let ce = - definition_entry ~opaque ~types:t ~polymorphic ~univs:ctx ~eff def - in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := @@ -946,7 +937,7 @@ let rec telescope = function let nf_evar_context sigma ctx = List.map (map_constr (Evarutil.nf_evar sigma)) ctx -let build_wellfounded (recname,pl,n,bl,arityc,body) polymorphic r measure notation = +let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -1057,7 +1048,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) polymorphic r measure notati let ty = it_mkProd_or_LetIn top_arity binders_rel in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~polymorphic ~types:ty ~univs (Evarutil.nf_evar !evdref body) in + let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1179,11 +1170,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind Option.map (List.map Proofview.V82.tactic) init_tac in let evd = Evd.from_ctx ctx in - let goal_kind = { locality = Global; - polymorphic = poly; - object_kind = DefinitionBody Fixpoint } - in - Lemmas.start_proof_with_initialization goal_kind + Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) @@ -1199,11 +1186,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let pl, ctx = Evd.universe_context ?names:pl evd in - let def_kind = { locality = local; - polymorphic = poly; - object_kind = Fixpoint } - in - ignore (List.map4 (declare_fix def_kind pl ctx) + ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1224,11 +1207,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n Option.map (List.map Proofview.V82.tactic) init_tac in let evd = Evd.from_ctx ctx in - let goal_kind = { locality = local; - polymorphic = poly; - object_kind = DefinitionBody CoFixpoint } - in - Lemmas.start_proof_with_initialization goal_kind + Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) @@ -1241,11 +1220,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let pl, ctx = Evd.universe_context ?names:pl evd in - let def_kind = { locality = local; - polymorphic = poly; - object_kind = CoFixpoint } - in - ignore (List.map4 (declare_fix def_kind pl ctx) + ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -1325,13 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns = fixl end in let ctx = Evd.evar_universe_context evd in - let object_kind = match fixkind with - | Obligations.IsFixpoint _ -> Fixpoint - | Obligations.IsCoFixpoint -> CoFixpoint - in - let kind = { locality = local; - polymorphic = p; - object_kind } + let kind = match fixkind with + | Obligations.IsFixpoint _ -> (local, p, Fixpoint) + | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind diff --git a/toplevel/command.mli b/toplevel/command.mli index f0651a98c..d35372429 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit (** {6 Definitions/Let} *) val interp_definition : - lident list option -> local_binder list -> polymorphic:bool -> red_expr option -> constr_expr -> + lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits @@ -55,10 +55,10 @@ val do_definition : Id.t -> definition_kind -> lident list option -> val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> Universes.universe_binders -> Impargs.manual_implicits -> - implicit_status -> Vernacexpr.inline -> variable Loc.located -> + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool -val do_assumptions : assumption_kind -> +val do_assumptions : locality * polymorphic * assumption_object_kind -> Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool (* val declare_assumptions : variable Loc.located list -> *) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index ceef929b9..aa1a489c2 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -490,7 +490,7 @@ let declare_definition prg = Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in let ce = definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~polymorphic:prg.prg_kind.polymorphic + ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in let () = progmap_remove prg in @@ -542,6 +542,7 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in + let (local,poly,kind) = first.prg_kind in let fixnames = first.prg_deps in let opaque = first.prg_opaque in let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in @@ -566,16 +567,14 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Stm.get_fix_exn () in - let def_kind = { first.prg_kind with object_kind = kind } in - let kns = List.map4 (!declare_fix_ref ~opaque def_kind ctx) + let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in - Lemmas.call_hook fix_exn first.prg_hook first.prg_kind.locality gr - first.prg_ctx; + Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; List.iter progmap_remove l; kn let decompose_lam_prod c ty = @@ -634,7 +633,7 @@ let declare_obligation prg obl body ty uctx = | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | force, Evar_kinds.Define opaque -> let opaque = not force && opaque in - let poly = prg.prg_kind.polymorphic in + let poly = pi2 prg.prg_kind in let ctx, body, ty, args = if get_shrink_obligations () && not poly then shrink_body body ty else [], body, ty, [||] @@ -792,15 +791,9 @@ let dependencies obls n = obls; !res -let goal_kind ~polymorphic = - { locality = Decl_kinds.Local; - polymorphic; - object_kind = Decl_kinds.DefinitionBody Decl_kinds.Definition } +let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition -let goal_proof_kind ~polymorphic = - { locality = Decl_kinds.Local; - polymorphic; - object_kind = Decl_kinds.Proof Decl_kinds.Lemma } +let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma let kind_of_obligation poly o = match o with @@ -898,7 +891,7 @@ in let _ = obls.(num) <- obl in let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = - if not prg.prg_kind.polymorphic then + if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) let evd = Evd.from_env (Global.env ()) in @@ -932,7 +925,7 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation prg.prg_kind.polymorphic (snd obl.obl_status) in + let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in @@ -976,13 +969,13 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = solve_by_tac obl.obl_name (evar_of_obligation obl) tac - prg.prg_kind.polymorphic (Evd.evar_universe_context evd) + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in let uctx = Evd.evar_context_universe_context ctx in 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 (prg.prg_kind.polymorphic) then ( + if def && not (pi2 prg.prg_kind) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in @@ -1078,12 +1071,7 @@ let show_term n = Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) -let default_definition_kind = - { locality = Global; - polymorphic = false; - object_kind = Definition } - -let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_kind) ?tactic +let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in @@ -1102,7 +1090,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_k | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ctx ?pl ?tactic ?(kind=default_definition_kind) ?(reduce=reduce) +let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Decls.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in diff --git a/toplevel/record.ml b/toplevel/record.ml index c98599d7f..de056fa9b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -426,7 +426,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity +let declare_class finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -441,11 +441,11 @@ let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity 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 ~polymorphic ~univs:ctx class_body in + 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 polymorphic then Univ.UContext.instance ctx else Univ.Instance.empty) 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 = @@ -453,8 +453,8 @@ let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity 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 ~polymorphic - ~univs:(if polymorphic then ctx else Univ.UContext.empty) proj_body + 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) @@ -469,7 +469,7 @@ let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite polymorphic 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e9fb8bd66..aa1999cf1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -469,22 +469,15 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - let goal_kind = { locality = local; - polymorphic = p; - object_kind = DefinitionBody k } - in - start_proof_and_print goal_kind [Some (lid,pl), (bl,t,None)] hook + start_proof_and_print (local,p,DefinitionBody k) + [Some (lid,pl), (bl,t,None)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> - let (evc,env)= get_current_context () in - Some (snd (Hook.get f_interp_redexp env evc r)) in - let def_kind = { locality = local; - polymorphic = p; - object_kind = k } - in - do_definition id def_kind pl bl red_option c typ_opt hook) + let (evc,env)= get_current_context () in + Some (snd (Hook.get f_interp_redexp env evc r)) in + do_definition id (local,p,k) pl bl red_option c typ_opt hook) let vernac_start_proof locality p kind l lettop = let local = enforce_locality_exp locality None in @@ -497,11 +490,7 @@ let vernac_start_proof locality p kind l lettop = if lettop then user_err ~hdr:"Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - let goal_kind = { locality = local; - polymorphic = p; - object_kind = Proof kind } - in - start_proof_and_print goal_kind l no_hook + start_proof_and_print (local, p, Proof kind) l no_hook let qed_display_script = ref true @@ -525,10 +514,7 @@ let vernac_exact_proof c = let vernac_assumption locality poly (local, kind) l nl = let local = enforce_locality_exp locality local in let global = local == Global in - let kind = {locality = local; - polymorphic = poly; - object_kind = kind } - in + let kind = local, poly, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> @@ -828,10 +814,10 @@ let vernac_identity_coercion locality poly local id qids qidt = (* Type classes *) -let vernac_instance abst locality ~polymorphic sup inst props pri = +let vernac_instance abst locality poly sup inst props pri = let global = not (make_section_locality locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global ~polymorphic sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri) let vernac_context poly l = if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom |