diff options
| author | Enrico Tassi | 2018-11-21 17:13:12 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-21 17:13:12 +0100 |
| commit | abcc20d6a3aebee36160cd17b1f80c56f39876f3 (patch) | |
| tree | 8c4da66c6a8e3ce515344db3752527cdff6ab2e0 /vernac | |
| parent | d6a53754602dd606644f90b3b6fb8fc82db6d373 (diff) | |
| parent | 002a974b66bc5b8524c8c045d6b9ec4f57aa7734 (diff) | |
Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/dune | 1 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/vernac/dune b/vernac/dune index 4673251002..45b567d631 100644 --- a/vernac/dune +++ b/vernac/dune @@ -3,7 +3,6 @@ (synopsis "Coq's Vernacular Language") (public_name coq.vernac) (wrapped false) - (flags :standard -open Gramlib) (libraries tactics parsing)) (rule diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index e6803443b3..befb4d7ccf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -29,7 +29,7 @@ exception EvaluatedError of Pp.t * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") |