diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4dd719e1f..dd0944cc4 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -11,7 +11,6 @@ open Names open Evd open Environ -open Misctypes open Libnames open Glob_term open Pattern @@ -142,10 +141,10 @@ val intern_constr_pattern : constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : reference -> GlobRef.t +val intern_reference : qualid -> GlobRef.t (** Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> glob_constr +val interp_reference : ltac_sign -> qualid -> glob_constr (** Interpret binders *) |