diff options
| author | herbelin | 2003-02-17 18:04:27 +0000 |
|---|---|---|
| committer | herbelin | 2003-02-17 18:04:27 +0000 |
| commit | cee9e38c3f2d6e1e639c7e6d63fed25c771115a9 (patch) | |
| tree | a50489edab726138353e75138d04e492feb585be | |
| parent | ebb4566be0ddaf482956a33ceb77176dbe955c28 (diff) | |
Affinement entree annot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3687 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constr.ml4 | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3413af8e25..eac6ce12f4 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -221,14 +221,18 @@ GEXTEND Gram let id2 = coerce_to_name lc2 in CProdN (loc, (id1::id2::idl, c)::bl, body) | "("; lc1 = lconstr; ")" -> lc1 - | c1 = annot; "->"; c2 = annot -> CArrow (loc, c1, c2) - | c1 = annot; "\\/"; c2 = annot -> CNotation (loc, "_ \\/ _", [c1;c2]) - | c1 = annot; "/\\"; c2 = annot -> CNotation (loc, "_ /\\ _", [c1;c2]) - | "~"; c = SELF -> CNotation (loc, "~ _", [c]) - | c1 = SELF; "=="; c2 = NEXT -> CNotation (loc, "_ == _", [c1;c2]) - | c1 = SELF; "="; c2 = NEXT -> CNotation (loc, "_ = _", [c1;c2]) - | c = constr LEVEL "4L" -> c - ] ] + | c1 = annot; "->"; c2 = annot -> CArrow (loc, c1, c2) ] + | RIGHTA + [ c1 = annot; "\\/"; c2 = annot -> CNotation (loc, "_ \\/ _", [c1;c2]) ] + | RIGHTA + [ c1 = annot; "/\\"; c2 = annot -> CNotation (loc, "_ /\\ _", [c1;c2]) ] + | RIGHTA + [ "~"; c = SELF -> CNotation (loc, "~ _", [c]) ] + | RIGHTA + [ c1 = SELF; "=="; c2 = NEXT -> CNotation (loc, "_ == _", [c1;c2]) ] + | RIGHTA + [ c1 = SELF; "="; c2 = NEXT -> CNotation (loc, "_ = _", [c1;c2]) ] + | [ c = constr LEVEL "4L" -> c ] ] ; product_annot_tail: [ [ ";"; idl = ne_name_comma_list; ":"; c = constr; |