From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/tacred.mli | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'pretyping/tacred.mli') 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 -- cgit v1.2.3