The Coq mailing list

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

Hi,

I am not making my way through with coqdep and coq_makefile. After running coqdep all I get is a list that shows no dependencies at all among different file names, see below:

Automata.vo Automata.glob Automata.v.beautified: Automata.v

Automata_finite.vo Automata_finite.glob Automata_finite.v.beautified: Automata_finite.v

Automata_stack.vo Automata_stack.glob Automata_stack.v.beautified: Automata_stack.v

Automata_turing.vo Automata_turing.glob Automata_turing.v.beautified: Automata_turing.v

Chomsky_hierarchy.vo Chomsky_hierarchy.glob Chomsky_hierarchy.v.beautified: Chomsky_hierarchy.v

Closure_properties_type_2.vo Closure_properties_type_2.glob Closure_properties_type_2.v.beautified: Closure_properties_type_2.v

Closure_properties_type_3.vo Closure_properties_type_3.glob Closure_properties_type_3.v.beautified: Closure_properties_type_3.v

Conversions_type_3.vo Conversions_type_3.glob Conversions_type_3.v.beautified: Conversions_type_3.v

Decidable_questions_type_3.vo Decidable_questions_type_3.glob Decidable_questions_type_3.v.beautified: Decidable_questions_type_3.v

Equivalences.vo Equivalences.glob Equivalences.v.beautified: Equivalences.v

Equivalences_type_0.vo Equivalences_type_0.glob Equivalences_type_0.v.beautified: Equivalences_type_0.v

Equivalences_type_2.vo Equivalences_type_2.glob Equivalences_type_2.v.beautified: Equivalences_type_2.v

Equivalences_type_3.vo Equivalences_type_3.glob Equivalences_type_3.v.beautified: Equivalences_type_3.v

Grammars.vo Grammars.glob Grammars.v.beautified: Grammars.v

Language_types.vo Language_types.glob Language_types.v.beautified: Language_types.v

Minimal.vo Minimal.glob Minimal.v.beautified: Minimal.v

Operations_type_2.vo Operations_type_2.glob Operations_type_2.v.beautified: Operations_type_2.v

Operations_type_3.vo Operations_type_3.glob Operations_type_3.v.beautified: Operations_type_3.v

Pumping_lemmas.vo Pumping_lemmas.glob Pumping_lemmas.v.beautified: Pumping_lemmas.v

Regular_expressions.vo Regular_expressions.glob Regular_expressions.v.beautified: Regular_expressions.v

Regular_sets.vo Regular_sets.glob Regular_sets.v.beautified: Regular_sets.v

String_sets.vo String_sets.glob String_sets.v.beautified: String_sets.v

Strings.vo Strings.glob Strings.v.beautified: Strings.v

Symbols.vo Symbols.glob Symbols.v.beautified: Symbols.v

What is the point that I am missing? Is there any tutorial with examples on how to use these tools correctly?

Thanks,

Marcus.