diff options
| -rw-r--r-- | tactics/declare.ml | 7 | ||||
| -rw-r--r-- | tactics/declare.mli | 9 | ||||
| -rw-r--r-- | tactics/hints.ml | 8 |
3 files changed, 6 insertions, 18 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 1e87a4b6ac..bfea15ac16 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -290,13 +290,6 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition - ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior) - ~name ?types (body,univs) = - let cb = definition_entry ?types ~univs ~opaque body in - declare_constant ~local ~name ~kind:Decls.(IsDefinition kind) - (DefinitionEntry cb) - (** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry diff --git a/tactics/declare.mli b/tactics/declare.mli index ae5c93db6a..93bb582751 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -70,15 +70,6 @@ val declare_private_constant -> Evd.side_effects constant_entry -> Constant.t * Evd.side_effects -val declare_definition - : ?opaque:bool - -> ?kind:Decls.definition_object_kind - -> ?local:import_status - -> name:Id.t - -> ?types:constr - -> constr Entries.in_universes_entry - -> Constant.t - (** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : diff --git a/tactics/hints.ml b/tactics/hints.ml index 90c43a1cb4..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 ~name: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)) |