diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index aa7604f5..e6065dda 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -14,7 +14,6 @@ open Evd open EConstr open Reductionops open Pattern -open Globnames open Locus open Univ open Ltac_pretype @@ -30,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Globnames.global_reference -> 'a +val error_not_evaluable : GlobRef.t -> 'a val evaluable_of_global_reference : - Environ.env -> Globnames.global_reference -> evaluable_global_reference + Environ.env -> GlobRef.t -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Globnames.global_reference + evaluable_global_reference -> GlobRef.t exception Redelimination @@ -88,10 +87,10 @@ val reduce_to_quantified_ind : env -> evar_map -> types -> (inductive * EInstan (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) val reduce_to_quantified_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val reduce_to_atomic_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val find_hnf_rectype : env -> evar_map -> types -> (inductive * EInstance.t) * constr list |