diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:32:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:32:24 +0000 |
| commit | 055466665e4c36b6cce376a27d8685a7a4f0846d (patch) | |
| tree | 770de75e90727956e1b93b8c5ec8cdf97076ef52 | |
| parent | 5fb9b0b82547eac276b5fb5d64a63396b557e3bc (diff) | |
Renommage command -> constr et changement des analyseurs syntaxiques de Grammar et Syntax
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@751 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/Ring.v | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index cc316e361..9045eab5f 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -9,35 +9,38 @@ Require Export Ring_abstract. Declare ML Module "ring". -Grammar tactic simple_tactic := - ring [ "Ring" comarg_list($arg) ] -> [(Ring ($LIST $arg))]. +Grammar tactic simple_tactic : Ast := + ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))]. Syntax tactic level 0: - ring [ (Ring ($LIST $lc)) ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] -| ring_e [ (Ring) ] -> ["Ring"]. + ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] +| ring_e [ << (Ring) >> ] -> ["Ring"]. -Grammar vernac vernac := +Grammar vernac vernac : Ast := addring [ "Add" "Ring" - comarg($a) comarg($aplus) comarg($amult) comarg($aone) - comarg($azero) comarg($aopp) comarg($aeq) comarg($t) - "[" ne_comarg_list($l) "]" "." ] + constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone) + constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t) + "[" ne_constrarg_list($l) "]" "." ] -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t ($LIST $l))] | addsemiring [ "Add" "Semi" "Ring" - comarg($a) comarg($aplus) comarg($amult) comarg($aone) - comarg($azero) comarg($aeq) comarg($t) - "[" ne_comarg_list($l) "]" "." ] + constrarg($a) constrarg($aplus) constrarg($amult) + constrarg($aone) constrarg($azero) constrarg($aeq) + constrarg($t) + "[" ne_constrarg_list($l) "]" "." ] -> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t ($LIST $l))] | addabstractring [ "Add" "Abstract" "Ring" - comarg($a) comarg($aplus) comarg($amult) comarg($aone) - comarg($azero) comarg($aopp) comarg($aeq) comarg($t) "." ] + constrarg($a) constrarg($aplus) constrarg($amult) + constrarg($aone) constrarg($azero) constrarg($aopp) + constrarg($aeq) constrarg($t) "." ] -> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)] | addabstractsemiring [ "Add" "Abstract" "Semi" "Ring" - comarg($a) comarg($aplus) comarg($amult) comarg($aone) - comarg($azero) comarg($aeq) comarg($t) "." ] + constrarg($a) constrarg($aplus) constrarg($amult) + constrarg($aone) constrarg($azero) constrarg($aeq) + constrarg($t) "." ] -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )] . |