Home My Page Projects Ott
Summary Activity Tracker

[#14195] coq error: The variable v_ is bound several times in pattern

Date:
2012-04-26 23:20
Priority:
3
State:
Open
Submitted by:
Nobody
Assigned to:
Nobody (None)
Summary:
coq error: The variable v_ is bound several times in pattern

Detailed description
Steps to reproduce:

File simplif.ott:

metavar var, x, y, z ::= {{ com Variable }}
{{ coq nat }}
indexvar index, i, j, k, n ::=
{{ coq nat }}

grammar

val, v :: val_ ::=
| x :: :: var

tm, t :: tm_ ::=
| x :: :: var
| t + t' :: :: plus
| </ ti * ti' // + // i /> :: :: etc

decl :: decl_ ::=
| </ xi = vi // i /> :: :: foo

formula :: formula_ ::=
| judgement :: :: judgement
| formula1 .. formulan :: :: dots

subrules
v <:: tm

defns
Job :: '' ::=

defn
v -- t' :: :: a :: a_ by

defn
t ++ t' :: :: b :: b_ by

</ vi -- ti // i />
-------------------- :: any
</ vi * ti // i /> ++ </ vj' * tj' // j />

defn
decl ** t :: :: c :: c_ by

</ vi -- ti // i />
----------------------- :: any
</ xi = vi // i /> ** t

$ ott -coq_expand_list_types false -i simplif.ott -o simplif.v
Ott version 0.21.2 distribution of Fri Jan 13 11:45:17 GMT 2012
warning: warning: indexvar "index" is primary so may give a name-clash

Definition rules: 2 good 0 bad
Definition rule clauses: 4 good 0 bad
$ coqc -I ~/code/ott_distro/coq simplif.vFile "./simplif.v", line 64, characters 62-72:
Error: The variable v_ is bound several times in pattern

Add A Comment: Notepad

Followup

No Followups Have Been Posted

Attached Files:

Changes:

No Changes Have Been Made to This Item