diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-02 10:18:48 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:17:34 +0100 |
| commit | d91a0c27402f0f19a30147bb9d87387ca2a91fd0 (patch) | |
| tree | b0ea13cb3186f8a405b3980c11571b19cc81f7aa /parsing | |
| parent | 2189505b6e50c9a9aa8e9d520c05461e59f18d04 (diff) | |
"Standardizing" the name LocalPatten into LocalRawPattern.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 47455f984..bbd494991 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -487,7 +487,7 @@ GEXTEND Gram | CPatCast (_, p, ty) -> (p, Some ty) | _ -> (p, None) in - [LocalPattern (!@loc, p, ty)] + [LocalRawPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18807113c..666797ba3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -249,7 +249,7 @@ GEXTEND Gram | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = - if List.exists (function LocalPattern _ -> true | _ -> false) bl + if List.exists (function LocalRawPattern _ -> true | _ -> false) bl then let c = CCast (!@loc, c, CastConv t) in (expand_pattern_binders mkCLambdaN bl c, None) |