diff options
| author | Jim Fehrle | 2020-10-11 18:39:16 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:15:35 -0700 |
| commit | b402adc12c00ba72046423d3a1737ccad517f70e (patch) | |
| tree | 1940efc064bf87b9b996a0e21eaa75e9b57605d4 /plugins/ssr | |
| parent | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff) | |
Rename operconstr -> term
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7b584b5159..77360052f8 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde GRAMMAR EXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 91cd5b251c..a49a5e8b28 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t) GRAMMAR EXTEND Gram GLOBAL: binder_constr; - ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]]; + ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } @@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: [ - [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> + [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> + | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in @@ -119,7 +119,7 @@ END GRAMMAR EXTEND Gram GLOBAL: closed_binder; closed_binder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] } ] ]; END |