diff options
| author | herbelin | 2001-03-23 23:25:31 +0000 |
|---|---|---|
| committer | herbelin | 2001-03-23 23:25:31 +0000 |
| commit | aef53771eb41a891d5808432f78ccdec156445c0 (patch) | |
| tree | 2eac40107d2be9d2592029c72e7f2615ecb704c7 /syntax | |
| parent | fae106f740d3d71555933cf416eec905c58f417e (diff) | |
Les règles d'affichage ajoutés dans le commit précédent avait le même nom que la règle pour command
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1484 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 19ec907910..2ee107c1bf 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -349,6 +349,6 @@ Syntax tactic level 8: tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ] - | tactic_to_constr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ] - | tactic_to_constr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ]. + | tactic_to_castedconstr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ] + | tactic_to_openconstr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ]. |