diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 44e5370e9..22df29b80 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -42,7 +42,7 @@ type 'a hint_ast = | Extern of Genarg.glob_generic_argument (* Hint Extern *) type hint -type raw_hint = constr * types * Univ.universe_context_set +type raw_hint = constr * types * Univ.ContextSet.t type 'a hints_path_atom_gen = | PathHints of 'a list @@ -146,7 +146,7 @@ type hint_info = (patvar list * constr_pattern) hint_info_gen type hint_term = | IsGlobRef of global_reference - | IsConstr of constr * Univ.universe_context_set + | IsConstr of constr * Univ.ContextSet.t type hints_entry = | HintsResolveEntry of @@ -193,7 +193,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> *) val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. [eapply] is true if this hint will be used only with EApply; @@ -211,7 +211,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint val make_apply_entry : env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product |