diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-02 19:02:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-02 19:02:41 +0000 |
| commit | 4fa8ff4c0463a85382351910522daf75bcdd6795 (patch) | |
| tree | 96eaff8d3ebac5af98f437662731f624d250cb2c /test-suite/success/CasesDep.v | |
| parent | c094d00faafb0a5c501323e9f3f9219db3effb68 (diff) | |
Remplacement de Syntactic Definition par Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/CasesDep.v')
| -rw-r--r-- | test-suite/success/CasesDep.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d0dc0f5c..3313827f1 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -76,7 +76,7 @@ Grammar constr constr1 := Definition equal := [A:Setoid] <[s:Setoid](Relation |s|)>let (S,R,e)=A in R. -Grammar constr constr1 := +Grammar constr constr1 := NONA equal [ constr0($c) "=" "%" "S" constr0($c2) ] -> [ (equal ? $c $c2) ]. @@ -111,7 +111,7 @@ End Maps. Notation ap := (explicit_ap ? ?). -Grammar constr constr8 := +Grammar constr constr8 := RIGHTA map_setoid [ constr7($c1) "=>" constr8($c2) ] -> [ (Map_setoid $c1 $c2) ]. |