list constructors conflict in Coq

Question

I have the following definitions in Coq:

Inductive list_variable : Type :=
| nil
| cons (s : string) (l : list_variable).

Fixpoint getElement (l : list_variable) (s : Variabile) (v : Address) {struct l} : Address :=
match l with
| nil => v
| str :: nil => (updateValues v ((updateState (updateState s "memPointer" (s("memPointer")+1)) str (s("memPointer"))) "memPointer") undef)
| str :: l => getElement l s v
end.

For some reason, the bottom and second line return Found a constructor of inductive type list while a constructor of list_variable is expected.

For reference, the long return on str::nil works fine in another place. It's for a memory-like simulation.

Any ideas as to why this happens?

Answer 1

The notation :: desugars to List.cons, whereas you want the constructor MyModule.cons. If you want to use ::, you must define a new notation for it:

Inductive list_variable : Type :=
| nil
| cons : ...
.

(* Redefine "::" for new list type *)
Infix "::" := cons.

If you intend to use the same notation for both list and list_variable, it will be necessary to manage notation scopes. Refer to the Coq manual, the section on notations.