_CoqProject

src/META.coq-equations.in
-I src
-I test-suite
-Q src Equations
-Q theories Equations
-I theories
-I examples

CAMLDEBUG = "-bin-annot -g -for-pack Equations -w -58"
COQDOCFLAGS = "-parse-comments -utf8 -interpolate"

src/equations_common.mli
src/equations_common.ml
src/ederive.ml
src/ederive.mli
src/sigma_types.mli
src/sigma_types.ml
src/subterm.mli
src/subterm.ml
src/eqdec.mli
src/eqdec.ml
src/depelim.mli
src/depelim.ml
src/syntax.mli
src/syntax.ml
src/context_map.mli
src/context_map.ml
src/simplify.mli
src/simplify.ml
src/splitting.mli
src/splitting.ml
src/covering.mli
src/covering.ml
src/principles_proofs.mli
src/principles_proofs.ml
src/principles.mli
src/principles.ml
src/equations.mli
src/equations.ml
src/noconf_hom.ml
src/noconf_hom.mli
src/noconf.ml
src/noconf.mli
src/extra_tactics.ml
src/extra_tactics.mli
src/g_equations.mlg
src/equations_plugin.mllib

theories/Init.v
theories/Signature.v
theories/CoreTactics.v

theories/Prop/SigmaNotations.v
theories/Prop/Logic.v
theories/Prop/Classes.v
theories/Prop/EqDec.v
theories/Prop/EqDecInstances.v
theories/Prop/Subterm.v
theories/Prop/DepElim.v
theories/Prop/Tactics.v
theories/Prop/Constants.v
theories/Prop/NoConfusion.v
theories/Prop/NoConfusion_UIP.v
theories/Prop/FunctionalInduction.v
theories/Prop/Loader.v
theories/Prop/Telescopes.v
theories/Prop/TransparentEquations.v
theories/Prop/OpaqueEquations.v
theories/Prop/NoCycle.v
theories/Prop/Equations.v

theories/Type/Logic.v
theories/Type/FunctionalExtensionality.v
theories/Type/Relation.v
theories/Type/Relation_Properties.v
theories/Type/WellFounded.v
theories/Type/Classes.v
theories/Type/EqDec.v
theories/Type/DepElim.v
theories/Type/Tactics.v
theories/Type/Subterm.v
theories/Type/Constants.v
theories/Type/EqDecInstances.v
theories/Type/NoConfusion.v
theories/Type/FunctionalInduction.v
theories/Type/Loader.v
theories/Type/Telescopes.v
theories/Type/WellFoundedInstances.v
theories/Type/All.v