The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Thanks Ralf. I tried that, however the output is:

$ make -f __makefile.coq clean

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `{ C:\Program Files (x86)\Coq\bin\coqtop -config | tr -d '\r' | tr '\n' '@'; }'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "useless_examples.v" > "useless_examples.v.d" || ( RV=$?; rm -f "useless_examples.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \useless_examples.v\ > \useless_examples.v.d\ || ( RV=$?; rm -f \useless_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "useless.v" > "useless.v.d" || ( RV=$?; rm -f "useless.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \useless.v\ > \useless.v.d\ || ( RV=$?; rm -f \useless.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "unitrules_examples.v" > "unitrules_examples.v.d" || ( RV=$?; rm -f "unitrules_examples.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \unitrules_examples.v\ > \unitrules_examples.v.d\ || ( RV=$?; rm -f \unitrules_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "unitrules.v" > "unitrules.v.d" || ( RV=$?; rm -f "unitrules.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \unitrules.v\ > \unitrules.v.d\ || ( RV=$?; rm -f \unitrules.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "misc_list.v" > "misc_list.v.d" || ( RV=$?; rm -f "misc_list.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \misc_list.v\ > \misc_list.v.d\ || ( RV=$?; rm -f \misc_list.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "misc_arith.v" > "misc_arith.v.d" || ( RV=$?; rm -f "misc_arith.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \misc_arith.v\ > \misc_arith.v.d\ || ( RV=$?; rm -f \misc_arith.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "inaccessible.v" > "inaccessible.v.d" || ( RV=$?; rm -f "inaccessible.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \inaccessible.v\ > \inaccessible.v.d\ || ( RV=$?; rm -f \inaccessible.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "emptyrules.v" > "emptyrules.v.d" || ( RV=$?; rm -f "emptyrules.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \emptyrules.v\ > \emptyrules.v.d\ || ( RV=$?; rm -f \emptyrules.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "cfg_examples.v" > "cfg_examples.v.d" || ( RV=$?; rm -f "cfg_examples.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \cfg_examples.v\ > \cfg_examples.v.d\ || ( RV=$?; rm -f \cfg_examples.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "cfg.v" > "cfg.v.d" || ( RV=$?; rm -f "cfg.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \cfg.v\ > \cfg.v.d\ || ( RV=$?; rm -f \cfg.v.d\; exit ${RV} )'

C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current "and_useless_inaccessible.v" > "and_useless_inaccessible.v.d" || ( RV=$?; rm -f "and_useless_inaccessible.v.d"; exit ${RV} )

/usr/bin/sh: -c: line 0: erro de sintaxe próximo do `token' não esperado `('

/usr/bin/sh: -c: line 0: `C:\Program Files (x86)\Coq\bin\coqdep -c -slash -R . Current \and_useless_inaccessible.v\ > \and_useless_inaccessible.v.d\ || ( RV=$?; rm -f \and_useless_inaccessible.v.d\; exit ${RV} )'

rm -f and_useless_inaccessible.vo cfg.vo cfg_examples.vo emptyrules.vo inaccessible.vo misc_arith.vo misc_list.vo unitrules.vo unitrules_examples.vo useless.vo useless_examples.vo and_useless_inaccessible.vi cfg.vi cfg_examples.vi emptyrules.vi inaccessible.vi misc_arith.vi misc_list.vi unitrules.vi unitrules_examples.vi useless.vi useless_examples.vi and_useless_inaccessible.g cfg.g cfg_examples.g emptyrules.g inaccessible.g misc_arith.g misc_list.g unitrules.g unitrules_examples.g useless.g useless_examples.g and_useless_inaccessible.v.d cfg.v.d cfg_examples.v.d emptyrules.v.d inaccessible.v.d misc_arith.v.d misc_list.v.d unitrules.v.d unitrules_examples.v.d useless.v.d useless_examples.v.d and_useless_inaccessible.v.beautified cfg.v.beautified cfg_examples.v.beautified emptyrules.v.beautified inaccessible.v.beautified misc_arith.v.beautified misc_list.v.beautified unitrules.v.beautified unitrules_examples.v.beautified useless.v.beautified useless_examples.v.beautified and_useless_inaccessible.v.old cfg.v.old cfg_examples.v.old emptyrules.v.old inaccessible.v.old misc_arith.v.old misc_list.v.old unitrules.v.old unitrules_examples.v.old useless.v.old useless_examples.v.old

rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob and_useless_inaccessible.glob cfg.glob cfg_examples.glob emptyrules.glob inaccessible.glob misc_arith.glob misc_list.glob unitrules.glob unitrules_examples.glob useless.glob useless_examples.glob and_useless_inaccessible.tex cfg.tex cfg_examples.tex emptyrules.tex inaccessible.tex misc_arith.tex misc_list.tex unitrules.tex unitrules_examples.tex useless.tex useless_examples.tex and_useless_inaccessible.g.tex cfg.g.tex cfg_examples.g.tex emptyrules.g.tex inaccessible.g.tex misc_arith.g.tex misc_list.g.tex unitrules.g.tex unitrules_examples.g.tex useless.g.tex useless_examples.g.tex all-mli.tex

rm -rf html mlihtml

2015-03-19 15:04 GMT+00:00 Ralf Jung <jung AT mpi-sws.org>:

Hi,

> Error: The file C:\Users\Marcus
> Ramos\Documents\Formalization\splitfiles/misc_arith.vo contains library
> misc_arith and not library Current.misc_arith
> make: *** [and_useless_inaccessible.vo] Error 1

Try running "make clean" first, to get rid of old files that were
compiled with different include paths.

Kind regards,
Ralf