diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-11 13:57:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-12 20:49:12 +0200 |
| commit | 116f8338b6fd60fdcf0f244772bcd6c82af5e333 (patch) | |
| tree | 84cdba7acbb30c37378f752601bac712c3e5d356 /grammar | |
| parent | e9aa3e6b70b1bab7138187733f6647b655a81b0b (diff) | |
Allowing simple ARGUMENT EXTEND not to mention their self type.
The TYPED AS clause was useless when defining a fresh generic argument.
Instead of having to write it mandatorily, we simply make it optional.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index c0be4598e..52119a963 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -75,8 +75,9 @@ let make_extend loc s cl wit = match cl with let declare_tactic_argument loc s (typ, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with - | `Uniform (typ, pr) -> - typ, pr, typ, pr, Some typ, pr + | `Uniform (otyp, pr) -> + let typ = match otyp with Some typ -> typ | None -> ExtraArgType s in + typ, pr, typ, pr, otyp, pr | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f in let glob = match g with @@ -180,23 +181,25 @@ EXTEND "END" -> declare_vernac_argument loc s pr l ] ] ; + argextend_specialized: + [ [ "RAW_TYPED"; "AS"; rawtyp = argtype; + "RAW_PRINTED"; "BY"; rawpr = LIDENT; + "GLOB_TYPED"; "AS"; globtyp = argtype; + "GLOB_PRINTED"; "BY"; globpr = LIDENT -> + (rawtyp, rawpr, globtyp, globpr) ] ] + ; argextend_header: - [ [ "TYPED"; "AS"; typ = argtype; - "PRINTED"; "BY"; pr = LIDENT; - f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; - g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; - h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] -> - (`Uniform (typ, pr), f, g, h) - | typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; + [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; - "RAW_TYPED"; "AS"; rawtyp = argtype; - "RAW_PRINTED"; "BY"; rawpr = LIDENT; - "GLOB_TYPED"; "AS"; globtyp = argtype; - "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (`Specialized (rawtyp, rawpr, globtyp, globpr, typ, pr), f, g, h) ] ] + special = OPT argextend_specialized -> + let repr = match special with + | None -> `Uniform (typ, pr) + | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) + in + (repr, f, g, h) ] ] ; argtype: [ "2" |