diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /pretyping/tacred.mli | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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 |