diff options
Diffstat (limited to 'tools/coqdep_lexer.mli')
| -rw-r--r-- | tools/coqdep_lexer.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 260586270..6b6e0da97 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -8,11 +8,15 @@ type mL_token = Use_module of string +type qualid = string list + type coq_token = - Require of string list list + Require of qualid list | RequireString of string | Declare of string list | Load of string + | AddLoadPath of string + | AddRecLoadPath of string * qualid exception Fin_fichier exception Syntax_error of int * int |