diff options
Diffstat (limited to 'grammar/argextend.ml4')
| -rw-r--r-- | grammar/argextend.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a02b7babc..cc378ceda 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -11,7 +11,6 @@ open Genarg open Q_util open Egramml -open Pcoq open Compat let loc = Loc.ghost @@ -264,7 +263,6 @@ let declare_vernac_argument loc s pr cl = ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } >> ] -open Vernacexpr open Pcoq open Pcaml open PcamlSig |