diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-19 18:31:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-19 18:31:27 +0000 |
| commit | 061fad5d12992b51a41aa593aefd99e9e820ea0b (patch) | |
| tree | caa1c2bf43ee1bdbadf3f19eed120566342bd4ca /theories | |
| parent | a13c56e9370364cb1dd50d4d3fb879af972eeb75 (diff) | |
Ajout d'un parseur d'entiers sous forme de pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Arith/Arith.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 05fa01f06..d5b4610a6 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -18,7 +18,7 @@ Grammar constr constr10 := natural_nat [ nat:number($c) ] -> [$c]. Grammar constr pattern := - natural_pat [ nat:number($c) ] -> [$c]. + natural_pat [ nat:pat_number($c) ] -> [$c]. Syntax constr level 0: |