diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 5 | ||||
| -rw-r--r-- | tactics/declare.ml | 170 | ||||
| -rw-r--r-- | tactics/declare.mli | 38 | ||||
| -rw-r--r-- | tactics/hints.ml | 8 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 3 | ||||
| -rw-r--r-- | tactics/leminv.ml | 3 |
6 files changed, 114 insertions, 113 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 662a2fc22c..09d7e0278a 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -13,7 +13,6 @@ module CVars = Vars open Util open Termops open EConstr -open Decl_kinds open Evarutil module RelDecl = Context.Rel.Declaration @@ -153,12 +152,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in - let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in + let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl + Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Proof_global.proof_entry_universes with diff --git a/tactics/declare.ml b/tactics/declare.ml index aa94ab5a25..e550e06471 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -11,21 +11,23 @@ (** This module is about the low-level declaration of logical objects *) open Pp -open CErrors open Util open Names -open Libnames -open Globnames -open Constr open Declarations open Entries +open Safe_typing open Libobject open Lib -open Impargs -open Safe_typing -open Cooking -open Decls -open Decl_kinds + +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + +let _ = CErrors.register_handler (function + | AlreadyDeclared (kind, id) -> + seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."] + | _ -> + raise CErrors.Unhandled) module NamedDecl = Context.Named.Declaration @@ -36,7 +38,7 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified type constant_obj = { cst_decl : Cooking.recipe option; (** Non-empty only when rebuilding a constant after a section *) - cst_kind : logical_kind; + cst_kind : Decls.logical_kind; cst_locl : import_status; } @@ -45,16 +47,14 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type constant_declaration = Evd.side_effects constant_entry * logical_kind - (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then - alreadydeclared (Id.print (basename sp) ++ str " already exists"); + raise (AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind + Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con); + Dumpglob.add_constant_kind con obj.cst_kind let cooking_info segment = let modlist = replacement_context () in @@ -70,32 +70,33 @@ let open_constant i ((sp,kn), obj) = | ImportNeedQualified -> () | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) + Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) + Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) let check_exists id = - if exists_name id then alreadydeclared (Id.print id ++ str " already exists") + if exists_name id then + raise (AlreadyDeclared (None, id)) let cache_constant ((sp,kn), obj) = (* Invariant: the constant must exist in the logical environment, except when redefining it when exiting a section. See [discharge_constant]. *) - let id = basename sp in + let id = Libnames.basename sp in let kn' = match obj.cst_decl with | None -> - if Global.exists_objlabel (Label.of_id (basename sp)) + if Global.exists_objlabel (Label.of_id (Libnames.basename sp)) then Constant.make1 kn - else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") + else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".") | Some r -> Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r in assert (Constant.equal kn' (Constant.make1 kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); + Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind + Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in @@ -103,7 +104,7 @@ let discharge_constant ((sp, kn), obj) = let info = cooking_info (section_segment_of_constant con) in (* This is a hack: when leaving a section, we lose the constant definition, so we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some { from; info } } + Some { obj with cst_decl = Some { Cooking.from; info } } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { @@ -127,8 +128,8 @@ let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f let update_tables c = - declare_constant_implicits c; - Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) + Impargs.declare_constant_implicits c; + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) let register_constant kn kind local = let o = inConstant { @@ -141,7 +142,7 @@ let register_constant kn kind local = update_tables kn let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in + let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] @@ -180,7 +181,7 @@ let cast_proof_entry e = (* This can actually happen, try compiling EqdepFacts for instance *) Monomorphic_entry (Univ.ContextSet.union ctx' ctx) | Polymorphic_entry _ -> - anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); + CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); in { const_entry_body = body; @@ -236,7 +237,7 @@ let get_roles export eff = in List.map map export -let define_constant ~side_effect id cd = +let define_constant ~side_effect ~name cd = let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let is_poly de = match de.proof_entry_universes with @@ -271,20 +272,20 @@ let define_constant ~side_effect id cd = | PrimitiveEntry e -> [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) in - let kn, eff = Global.add_constant ~side_effect ~in_section id decl in + let kn, eff = Global.add_constant ~side_effect ~in_section name decl in kn, eff, export -let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = - let () = check_exists id in - let kn, (), export = define_constant ~side_effect:PureEntry id cd in +let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = + let () = check_exists name in + let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) = - let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in - let () = assert (List.is_empty export) in +let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd = + let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in + let () = assert (CList.is_empty export) in let () = register_constant kn kind local in let seff_roles = match role with | None -> Cmap.empty @@ -293,34 +294,25 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) - id ?types (body,univs) = - let cb = - definition_entry ?types ~univs ~opaque body - in - declare_constant ~local id - (DefinitionEntry cb, Decl_kinds.IsDefinition kind) - (** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry let cache_variable ((sp,_),o) = match o with | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(path,d,kind)) -> + | Inr (id,(path,d),kind) -> (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); + if Decls.variable_exists id then + raise (AlreadyDeclared (None, id)); let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> let () = Global.push_named_assum ((id,typ,poly),univs) in - let impl = if impl then Implicit else Explicit in + let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in impl, true, poly, univs | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a @@ -345,20 +337,20 @@ let cache_variable ((sp,_),o) = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (id, se) in - Explicit, de.proof_entry_opaque, + Decl_kinds.Explicit, de.proof_entry_opaque, poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + Nametab.push (Nametab.Until 1) (Libnames.restrict_path 0 sp) (GlobRef.VarRef id); add_section_variable ~name:id ~kind:impl ~poly univs; - add_variable_data id {path;opaque;univs;poly;kind} + Decls.(add_variable_data id {path;opaque;univs;poly;kind}) let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) + | Inr (id,_,_) -> + if Decls.variable_polymorphic id then None + else Some (Inl (Decls.variable_context id)) | Inl _ -> Some o type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union + (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with @@ -367,22 +359,22 @@ let inVariable : variable_obj -> obj = classify_function = (fun _ -> Dispose) } (* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope Evd.empty (VarRef id); +let declare_variable ~name ~kind obj = + let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in + Impargs.declare_var_implicits name; + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name); oname (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); done) mie.mind_entry_inds let inductive_names sp kn mie = - let (dp,_) = repr_path sp in + let (dp,_) = Libnames.repr_path sp in let kn = Global.mind_of_delta_kn kn in let names, _ = List.fold_left @@ -394,11 +386,11 @@ let inductive_names sp kn mie = let sp = Libnames.make_path dp l in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) (names, 1) ind.mind_entry_consnames in let sp = Libnames.make_path dp ind.mind_entry_typename in - ((sp, IndRef ind_p) :: names, n+1)) + ((sp, GlobRef.IndRef ind_p) :: names, n+1)) ([], 0) mie.mind_entry_inds in names @@ -412,8 +404,8 @@ let open_inductive i ((sp,kn),mie) = let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in - List.iter check_exists (List.map (fun p -> basename (fst p)) names); - let id = basename sp in + List.iter check_exists (List.map (fun p -> Libnames.basename (fst p)) names); + let id = Libnames.basename sp in let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in @@ -428,7 +420,7 @@ let discharge_inductive ((sp,kn),mie) = let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; + mind_entry_arity = Constr.mkProp; mind_entry_template = false; mind_entry_consnames = mie.mind_entry_consnames; mind_entry_lc = [] @@ -480,7 +472,7 @@ let inPrim : (Projection.Repr.t * Constant.t) -> obj = let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let id = Label.to_id label in + let name = Label.to_id label in let univs, u = match univs with | Monomorphic_entry _ -> (* Global constraints already defined through the inductive *) @@ -491,11 +483,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let term = Vars.subst_instance_constr u term in let types = Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in declare_primitive_projection p cst - let declare_projections univs mind = let env = Global.env () in let mib = Environ.lookup_mind mind env in @@ -515,11 +506,11 @@ let declare_projections univs mind = let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in + | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive mie) in let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in - declare_mib_implicits mind; + Impargs.declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim @@ -529,7 +520,7 @@ let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition.") + | [] -> CErrors.anomaly (Pp.str "no recursive definition.") | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" @@ -544,7 +535,7 @@ let fixpoint_message indexes l = let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition.") + | [] -> CErrors.anomaly (Pp.str "No corecursive definition.") | [id] -> Id.print id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are corecursively defined")) @@ -586,9 +577,9 @@ type universe_source = type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list -let check_exists sp = +let check_exists_universe sp = if Nametab.exists_universe sp then - alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") + raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) else () let qualify_univ i dp src id = @@ -601,19 +592,19 @@ let qualify_univ i dp src id = let do_univ_name ~check i dp src (id,univ) = let i, sp = qualify_univ i dp src id in - if check then check_exists sp; + if check then check_exists_universe sp; Nametab.push_universe i sp univ let cache_univ_names ((sp, _), (src, univs)) = let depth = sections_depth () in - let dp = pop_dirpath_n depth (dirpath sp) in + let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs + List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs let discharge_univ_names = function | _, (BoundUniv, _) -> None @@ -633,12 +624,13 @@ let declare_univ_binders gr pl = if Global.is_polymorphic gr then () else - let l = match gr with + let l = let open GlobRef in match gr with | ConstRef c -> Label.to_id @@ Constant.label c | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> - anomaly ~label:"declare_univ_binders" + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on an constructor reference") in let univs = Id.Map.fold (fun id univ univs -> @@ -652,7 +644,7 @@ let do_universe ~poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in @@ -672,13 +664,13 @@ let do_constraint ~poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly p p' = if poly then () else if p || p' then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") diff --git a/tactics/declare.mli b/tactics/declare.mli index 1f72fff30e..f2d23fb319 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Decl_kinds (** This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions @@ -31,15 +30,17 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry -val declare_variable : variable -> variable_declaration -> Libobject.object_name +val declare_variable + : name:variable + -> kind:Decls.logical_kind + -> variable_declaration + -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = Evd.side_effects constant_entry * logical_kind - (* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> @@ -54,16 +55,20 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) -val declare_constant : - ?local:import_status -> Id.t -> constant_declaration -> Constant.t - -val declare_private_constant : - ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects - -val declare_definition : - ?opaque:bool -> ?kind:definition_object_kind -> - ?local:import_status -> Id.t -> ?types:constr -> - constr Entries.in_universes_entry -> Constant.t +val declare_constant + : ?local:import_status + -> name:Id.t + -> kind:Decls.logical_kind + -> Evd.side_effects constant_entry + -> Constant.t + +val declare_private_constant + : ?role:Evd.side_effect_role + -> ?local:import_status + -> name:Id.t + -> kind:Decls.logical_kind + -> Evd.side_effects constant_entry + -> Constant.t * Evd.side_effects (** Since transparent constants' side effects are globally declared, we * need that *) @@ -93,3 +98,6 @@ val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit val do_universe : poly:bool -> lident list -> unit val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit + +(* Used outside this module only in indschemes *) +exception AlreadyDeclared of (string option * Id.t) diff --git a/tactics/hints.ml b/tactics/hints.ml index 3a3a6b94dc..8d1c536db6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1315,12 +1315,16 @@ let project_hint ~poly pri l2r r = let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in - let id = + let name = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition id (c,ctx) in + let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in + let c = Declare.declare_constant + ~local:Declare.ImportDefaultBehavior + ~name ~kind:Decls.(IsDefinition Definition) cb + in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e01f3ab961..e2ef05461b 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,7 +22,6 @@ open Declarations open Constr open CErrors open Util -open Decl_kinds open Pp (**********************************************************************) @@ -136,7 +135,7 @@ let define internal role id c poly univs = proof_entry_inline_code = false; proof_entry_feedback = None; } in - let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in let () = match internal with | InternalTacticRequest -> () | _-> Declare.definition_message id diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e242b10d33..2af3947dd1 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,7 +27,6 @@ open Tacmach.New open Clenv open Tacticals.New open Tactics -open Decl_kinds open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -236,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.univ_entry ~poly sigma in let entry = Declare.definition_entry ~univs invProof in - let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in + let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in () (* inv_op = Inv (derives de complete inv. lemma) |