diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 5 | ||||
| -rw-r--r-- | interp/topconstr.mli | 5 |
2 files changed, 8 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 12ce52d1b5..a6b4b1b0ab 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1001,7 +1001,6 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr - type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast @@ -1015,6 +1014,10 @@ type include_ast = | CIMTE of module_type_ast * module_type_ast list | CIME of module_ast * module_ast list +type 'a module_signature = + | Enforce of 'a (* ... : T *) + | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + let loc_of_notation f loc (args,_) ntn = if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc) else snd (Util.unloc (f (List.hd args))) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1b6514a658..1c0b207eab 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -245,7 +245,6 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr - type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast @@ -259,5 +258,9 @@ type include_ast = | CIMTE of module_type_ast * module_type_ast list | CIME of module_ast * module_ast list +type 'a module_signature = + | Enforce of 'a (* ... : T *) + | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int |