_CoqProject

src/META.coq-mtac2.in
COQMF_WARN = "-warn-error +a-3-23"
CAMLDEBUG = "-g"
-arg -bt
-I src
-R theories Mtac2
-Q tests Mtac2Tests
-arg "-w -unrecognized-unicode"
src/metaCoqInit.mlg
src/metaCoqInstr.mli
src/constrs.ml
src/constrs.mli
src/mtacNames.ml
src/mtacNames.mli
src/mConstr.ml
src/mConstr.mli
src/run.ml
src/run.mli
src/metaCoqInterp.ml
src/metaCoqInterp.mli
src/metaCoqTactic.mlg
src/MetaCoqPlugin.mlpack
theories/lib/Logic.v
theories/lib/Specif.v
theories/lib/Datatypes.v
theories/lib/List.v
theories/lib/Utils.v
theories/intf/Sorts.v
theories/Base.v
theories/DecomposeApp.v
theories/tactics/TacticsBase.v
theories/tactics/Tactics.v
theories/tactics/ImportedTactics.v
theories/tactics/IntroPatt.v
theories/tactics/CompoundTactics.v
theories/tactics/ConstrSelector.v
theories/tactics/Ttactics.v
theories/Mtac2.v
theories/intf/MTele.v
theories/meta/MTeleMatchDef.v
theories/meta/MTeleMatch.v
theories/meta/MFixDef.v
theories/meta/MFix.v
theories/ideas/SumRun.v
theories/Pattern.v
theories/intf/Dyn.v
theories/intf/Name.v
theories/intf/Exceptions.v
theories/intf/Reduction.v
theories/intf/DeclarationDefs.v
theories/intf/Unification.v
theories/intf/Case.v
theories/intf/Goals.v
theories/intf/Lift.v
theories/intf/Tm_kind.v
theories/intf/M.v
theories/meta/Exhaustive.v
theories/ideas/Abstract.v
theories/ideas/DepDestruct.v
theories/ideas/SubgoalsStrict.v
theories/ideas/StaticApply.v
theories/ideas/Transport.v