diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 9 | ||||
| -rw-r--r-- | tactics/hints.mli | 13 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 6 |
4 files changed, 17 insertions, 14 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ed92a85a12..9e66e8668f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -482,8 +482,7 @@ let make_resolve_hyp env sigma st only_classes pri decl = let keep = not only_classes || is_class in if keep then let id = GlobRef.VarRef id in - let name = PathHints [id] in - (make_resolves env sigma pri ~name ~check:false (IsGlobRef id)) + make_resolves env sigma pri id else [] let make_hints g (modes,st) only_classes sign = diff --git a/tactics/hints.ml b/tactics/hints.ml index fe3efef7c5..68229dbe26 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1347,6 +1347,10 @@ let add_hints ~locality dbnames h = | HintsExternEntry (info, tacexp) -> add_externs info tacexp ~local ~superglobal dbnames +let hint_globref gr = IsGlobRef gr + +let hint_constr (c, diff) = IsConstr (c, diff) + let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> match EConstr.kind sigma lem with @@ -1365,8 +1369,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun lem -> make_resolves env sigma (eapply, true) empty_hint_info ~check:true lem) lems -let make_resolves env sigma info ~check ?name hint = - make_resolves env sigma (true, false) info ~check ?name hint +let make_resolves env sigma info hint = + let name = PathHints [hint] in + make_resolves env sigma (true, false) info ~check:false ~name (IsGlobRef hint) let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/hints.mli b/tactics/hints.mli index dd22cff10b..3d4d9c7970 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -167,9 +167,7 @@ type hint_db = Hint_db.t type hnf = bool -type hint_term = - | IsGlobRef of GlobRef.t - | IsConstr of constr * Univ.ContextSet.t option [@ocaml.deprecated "Declare a hint constant instead"] +type hint_term type hints_entry = | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list @@ -199,8 +197,10 @@ val current_pure_db : unit -> hint_db list val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit -val prepare_hint : bool (* Check no remaining evars *) -> - env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) +val hint_globref : GlobRef.t -> hint_term + +val hint_constr : constr * Univ.ContextSet.t option -> hint_term +[@ocaml.deprecated "Declare a hint constant instead"] (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product @@ -210,8 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> has missing arguments. *) val make_resolves : - env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom -> - hint_term -> hint_entry list + env -> evar_map -> hint_info -> GlobRef.t -> hint_entry list (** [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 9164a4ff26..b16153a39e 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -100,9 +100,9 @@ let check_scheme kind ind = Option.has_some (lookup_scheme kind ind) let define internal role id c poly univs = let id = compute_name internal id in - let ctx = UState.minimize univs in - let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in - let univs = UState.univ_entry ~poly ctx in + let uctx = UState.minimize univs in + let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst uctx) c in + let univs = UState.univ_entry ~poly uctx in !declare_definition_scheme ~internal ~univs ~role ~name:id c (* Assumes that dependencies are already defined *) |