diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 11:36:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:57 +0100 |
| commit | c1cab3ba606f7034f2785f06c0d3892bca3976cf (patch) | |
| tree | 19918420f7e4b64be31953dae8f51c981e638f4a /plugins/ssr | |
| parent | 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (diff) | |
Removing cumbersome location in multiple patterns.
This is to have a better symmetry between CCases and GCases.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 3efb7b914..4f530a0ae 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> |