aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
authorMaxime Dénès2016-07-03 18:54:06 +0200
committerMaxime Dénès2016-07-03 18:54:06 +0200
commite278d031a1d9a7bf3de463d3d415065299c99395 (patch)
treeddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /grammar
parentd7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff)
parent3ce70f21a18cc19e720e8ac54b93652527881942 (diff)
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.mlp4
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index eaaa7f0256..d0ab5d8037 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -180,8 +180,8 @@ let declare_vernac_argument loc s pr cl =
<:str_item< do {
Pptactic.declare_extra_genarg_pprule $wit$
$pr_rules$
- (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer"))
- (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
+ (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer"))
+ (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer")) }
>> ]
open Pcaml