diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index c9b139ac9..37531af21 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,7 +15,7 @@ open Closure open Glob_term open Termops open Pattern -open Libnames +open Globnames open Locus type reduction_tactic_error = @@ -29,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Libnames.global_reference -> 'a +val error_not_evaluable : Globnames.global_reference -> 'a val evaluable_of_global_reference : - Environ.env -> Libnames.global_reference -> evaluable_global_reference + Environ.env -> Globnames.global_reference -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Libnames.global_reference + evaluable_global_reference -> Globnames.global_reference exception Redelimination |