updated .gitignore

1 files changed, 24 insertions, 326 deletions

diff --git a/.gitignore b/.gitignore
index 9db2580..75736be 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,344 +1,42 @@
+*.annot
+*.cmt
+*.cmti
+*.vtlog
+*.zlog
+*.cache
+*.cmi
+*.cmo
+*.cmx
+*.cmxs
+*.cmxa
+*.ml.d
+*.mli.d
+*.ml4.d
+*.native
+*.o
+*.a
+*.glob
+*.vo
+*.v.d
+*.aux
+*.mlpack.d
 src/Makefile
-src/Misc.glob
-src/Misc.v.d
-src/Misc.vo
-src/NSMTCoq_Misc.cmi
-src/NSMTCoq_Misc.cmx
-src/NSMTCoq_Misc.cmxs
-src/NSMTCoq_Misc.native
-src/NSMTCoq_Misc.o
-src/NSMTCoq_SMTCoq.cmi
-src/NSMTCoq_SMTCoq.cmx
-src/NSMTCoq_SMTCoq.cmxs
-src/NSMTCoq_SMTCoq.native
-src/NSMTCoq_SMTCoq.o
-src/NSMTCoq_SMT_terms.cmi
-src/NSMTCoq_SMT_terms.cmx
-src/NSMTCoq_SMT_terms.cmxs
-src/NSMTCoq_SMT_terms.native
-src/NSMTCoq_SMT_terms.o
-src/NSMTCoq_State.cmi
-src/NSMTCoq_State.cmx
-src/NSMTCoq_State.cmxs
-src/NSMTCoq_State.native
-src/NSMTCoq_State.o
-src/NSMTCoq_Trace.cmi
-src/NSMTCoq_Trace.cmx
-src/NSMTCoq_Trace.cmxs
-src/NSMTCoq_Trace.native
-src/NSMTCoq_Trace.o
-src/SMTCoq.glob
-src/SMTCoq.v.d
-src/SMTCoq.vo
-src/SMT_terms.glob
-src/SMT_terms.v.d
-src/SMT_terms.vo
-src/State.glob
-src/State.v.d
-src/State.vo
-src/Trace.glob
-src/Trace.v.d
-src/Trace.vo
-src/cnf/Cnf.glob
-src/cnf/Cnf.v.d
-src/cnf/Cnf.vo
-src/cnf/NSMTCoq_cnf_Cnf.cmi
-src/cnf/NSMTCoq_cnf_Cnf.cmx
-src/cnf/NSMTCoq_cnf_Cnf.cmxs
-src/cnf/NSMTCoq_cnf_Cnf.native
-src/cnf/NSMTCoq_cnf_Cnf.o
-src/euf/Euf.glob
-src/euf/Euf.v.d
-src/euf/Euf.vo
-src/euf/NSMTCoq_euf_Euf.cmi
-src/euf/NSMTCoq_euf_Euf.cmx
-src/euf/NSMTCoq_euf_Euf.cmxs
-src/euf/NSMTCoq_euf_Euf.native
-src/euf/NSMTCoq_euf_Euf.o
 src/extraction/.Makefile.swp
-src/extraction/extrNative.cmi
-src/extraction/extrNative.cmx
-src/extraction/extrNative.o
-src/extraction/sat_checker.cmi
-src/extraction/sat_checker.cmx
-src/extraction/sat_checker.o
-src/extraction/smt_checker.cmi
-src/extraction/smt_checker.cmx
-src/extraction/smt_checker.o
 src/extraction/smtcoq
-src/extraction/smtcoq.cmi
-src/extraction/smtcoq.cmx
-src/extraction/smtcoq.o
-src/extraction/verit_checker.cmi
-src/extraction/verit_checker.cmx
-src/extraction/verit_checker.o
-src/extraction/zchaff_checker.cmi
-src/extraction/zchaff_checker.cmx
-src/extraction/zchaff_checker.o
-src/lia/Lia.glob
-src/lia/Lia.v.d
-src/lia/Lia.vo
-src/lia/NSMTCoq_lia_Lia.cmi
-src/lia/NSMTCoq_lia_Lia.cmx
-src/lia/NSMTCoq_lia_Lia.cmxs
-src/lia/NSMTCoq_lia_Lia.native
-src/lia/NSMTCoq_lia_Lia.o
-src/lia/lia.cmi
-src/lia/lia.cmx
-src/lia/lia.ml.d
-src/lia/lia.mli.d
-src/lia/lia.o
-src/smtcoq.a
-src/smtcoq.cmxa
-src/smtcoq_plugin.cmi
-src/smtcoq_plugin.cmo
-src/smtcoq_plugin.cmx
-src/smtcoq_plugin.cmxs
 src/smtcoq_plugin.ml4
-src/smtcoq_plugin.ml4.d
-src/smtcoq_plugin.o
-src/smtlib2/smtlib2_ast.cmi
-src/smtlib2/smtlib2_ast.cmx
-src/smtlib2/smtlib2_ast.ml.d
-src/smtlib2/smtlib2_ast.mli.d
-src/smtlib2/smtlib2_ast.o
-src/smtlib2/smtlib2_genConstr.cmi
-src/smtlib2/smtlib2_genConstr.cmx
-src/smtlib2/smtlib2_genConstr.ml.d
-src/smtlib2/smtlib2_genConstr.mli.d
-src/smtlib2/smtlib2_genConstr.o
-src/smtlib2/smtlib2_lex.cmi
-src/smtlib2/smtlib2_lex.cmx
-src/smtlib2/smtlib2_lex.ml
-src/smtlib2/smtlib2_lex.ml.d
-src/smtlib2/smtlib2_lex.o
-src/smtlib2/smtlib2_parse.cmi
-src/smtlib2/smtlib2_parse.cmx
 src/smtlib2/smtlib2_parse.ml
-src/smtlib2/smtlib2_parse.ml.d
-src/smtlib2/smtlib2_parse.mli.d
-src/smtlib2/smtlib2_parse.o
-src/smtlib2/smtlib2_util.cmi
-src/smtlib2/smtlib2_util.cmx
-src/smtlib2/smtlib2_util.ml.d
-src/smtlib2/smtlib2_util.mli.d
-src/smtlib2/smtlib2_util.o
-src/spl/Arithmetic.glob
-src/spl/Arithmetic.v.d
-src/spl/Arithmetic.vo
-src/spl/Assumptions.glob
-src/spl/Assumptions.v.d
-src/spl/Assumptions.vo
-src/spl/NSMTCoq_spl_Arithmetic.cmi
-src/spl/NSMTCoq_spl_Arithmetic.cmx
-src/spl/NSMTCoq_spl_Arithmetic.cmxs
-src/spl/NSMTCoq_spl_Arithmetic.native
-src/spl/NSMTCoq_spl_Arithmetic.o
-src/spl/NSMTCoq_spl_Assumptions.cmi
-src/spl/NSMTCoq_spl_Assumptions.cmx
-src/spl/NSMTCoq_spl_Assumptions.cmxs
-src/spl/NSMTCoq_spl_Assumptions.native
-src/spl/NSMTCoq_spl_Assumptions.o
-src/spl/NSMTCoq_spl_Operators.cmi
-src/spl/NSMTCoq_spl_Operators.cmx
-src/spl/NSMTCoq_spl_Operators.cmxs
-src/spl/NSMTCoq_spl_Operators.native
-src/spl/NSMTCoq_spl_Operators.o
-src/spl/NSMTCoq_spl_Syntactic.cmi
-src/spl/NSMTCoq_spl_Syntactic.cmx
-src/spl/NSMTCoq_spl_Syntactic.cmxs
-src/spl/NSMTCoq_spl_Syntactic.native
-src/spl/NSMTCoq_spl_Syntactic.o
-src/spl/Operators.glob
-src/spl/Operators.v.d
-src/spl/Operators.vo
-src/spl/Syntactic.glob
-src/spl/Syntactic.v.d
-src/spl/Syntactic.vo
-src/trace/coqTerms.cmi
-src/trace/coqTerms.cmx
-src/trace/coqTerms.ml.d
-src/trace/coqTerms.mli.d
-src/trace/coqTerms.o
-src/trace/satAtom.cmi
-src/trace/satAtom.cmx
-src/trace/satAtom.ml.d
-src/trace/satAtom.mli.d
-src/trace/satAtom.o
-src/trace/smtAtom.cmi
-src/trace/smtAtom.cmx
-src/trace/smtAtom.ml.d
-src/trace/smtAtom.mli.d
-src/trace/smtAtom.o
-src/trace/smtCertif.cmi
-src/trace/smtCertif.cmx
-src/trace/smtCertif.ml.d
-src/trace/smtCertif.mli.d
-src/trace/smtCertif.o
-src/trace/smtCnf.cmi
-src/trace/smtCnf.cmx
-src/trace/smtCnf.ml.d
-src/trace/smtCnf.mli.d
-src/trace/smtCnf.o
-src/trace/smtCommands.cmi
-src/trace/smtCommands.cmx
-src/trace/smtCommands.ml.d
-src/trace/smtCommands.mli.d
-src/trace/smtCommands.o
-src/trace/smtForm.cmi
-src/trace/smtForm.cmx
-src/trace/smtForm.ml.d
-src/trace/smtForm.mli.d
-src/trace/smtForm.o
-src/trace/smtMisc.cmi
-src/trace/smtMisc.cmx
-src/trace/smtMisc.ml.d
-src/trace/smtMisc.mli.d
-src/trace/smtMisc.o
-src/trace/smtTrace.cmi
-src/trace/smtTrace.cmx
-src/trace/smtTrace.ml.d
-src/trace/smtTrace.mli.d
-src/trace/smtTrace.o
-src/verit/verit.cmi
-src/verit/verit.cmx
-src/verit/verit.ml.d
-src/verit/verit.mli.d
-src/verit/verit.o
-src/verit/veritLexer.cmi
-src/verit/veritLexer.cmx
-src/verit/veritLexer.ml
-src/verit/veritLexer.ml.d
-src/verit/veritLexer.o
-src/verit/veritParser.cmi
-src/verit/veritParser.cmx
 src/verit/veritParser.ml
-src/verit/veritParser.ml.d
-src/verit/veritParser.mli.d
-src/verit/veritParser.o
-src/verit/veritSyntax.cmi
-src/verit/veritSyntax.cmx
-src/verit/veritSyntax.ml.d
-src/verit/veritSyntax.mli.d
-src/verit/veritSyntax.o
-src/versions/native/NSMTCoq_versions_native_Structures.cmi
-src/versions/native/NSMTCoq_versions_native_Structures.cmx
-src/versions/native/NSMTCoq_versions_native_Structures.cmxs
-src/versions/native/NSMTCoq_versions_native_Structures.native
-src/versions/native/NSMTCoq_versions_native_Structures.o
-src/versions/native/Structures.glob
 src/versions/native/Structures.v
-src/versions/native/Structures.v.d
-src/versions/native/Structures.vo
-src/versions/native/structures.cmi
-src/versions/native/structures.cmx
-src/versions/native/structures.ml.d
-src/versions/native/structures.mli.d
-src/versions/native/structures.o
-src/zchaff/cnfParser.cmi
-src/zchaff/cnfParser.cmx
-src/zchaff/cnfParser.ml.d
-src/zchaff/cnfParser.mli.d
-src/zchaff/cnfParser.o
-src/zchaff/satParser.cmi
-src/zchaff/satParser.cmx
-src/zchaff/satParser.ml.d
-src/zchaff/satParser.mli.d
-src/zchaff/satParser.o
-src/zchaff/zchaff.cmi
-src/zchaff/zchaff.cmx
-src/zchaff/zchaff.ml.d
-src/zchaff/zchaff.mli.d
-src/zchaff/zchaff.o
-src/zchaff/zchaffParser.cmi
-src/zchaff/zchaffParser.cmx
-src/zchaff/zchaffParser.ml.d
-src/zchaff/zchaffParser.mli.d
-src/zchaff/zchaffParser.o
-src/.Misc.aux
-src/.SMTCoq.aux
-src/.SMT_terms.aux
-src/.State.aux
-src/.Trace.aux
-src/.lia.cache
-src/cnf/.Cnf.aux
-src/euf/.Euf.aux
-src/g_smtcoq.cmi
-src/g_smtcoq.cmo
-src/g_smtcoq.cmx
 src/g_smtcoq.ml4
-src/g_smtcoq.ml4.d
-src/g_smtcoq.o
-src/lia/.Lia.aux
-src/lia/lia.cmo
 src/smtcoq_plugin.mlpack
-src/smtcoq_plugin.mlpack.d
-src/smtlib2/smtlib2_ast.cmo
-src/smtlib2/smtlib2_genConstr.cmo
-src/smtlib2/smtlib2_lex.cmo
-src/smtlib2/smtlib2_parse.cmo
+src/smtlib2/smtlib2_lex.ml
 src/smtlib2/smtlib2_parse.mli
-src/smtlib2/smtlib2_util.cmo
-src/spl/.Arithmetic.aux
-src/spl/.Assumptions.aux
-src/spl/.Operators.aux
-src/spl/.Syntactic.aux
-src/trace/coqTerms.cmo
-src/trace/satAtom.cmo
-src/trace/smtAtom.cmo
-src/trace/smtCertif.cmo
-src/trace/smtCnf.cmo
-src/trace/smtCommands.cmo
-src/trace/smtForm.cmo
-src/trace/smtMisc.cmo
-src/trace/smtTrace.cmo
-src/verit/verit.cmo
-src/verit/veritLexer.cmo
-src/verit/veritParser.cmo
+src/verit/veritLexer.ml
 src/verit/veritParser.mli
-src/verit/veritSyntax.cmo
-src/versions/standard/.Structures.aux
-src/versions/standard/Array/.PArray.aux
-src/versions/standard/Array/PArray.glob
 src/versions/standard/Array/PArray.v
-src/versions/standard/Array/PArray.v.d
-src/versions/standard/Array/PArray.vo
-src/versions/standard/Int63/.Int63.aux
-src/versions/standard/Int63/.Int63Axioms.aux
-src/versions/standard/Int63/.Int63Native.aux
-src/versions/standard/Int63/.Int63Op.aux
-src/versions/standard/Int63/.Int63Properties.aux
-src/versions/standard/Int63/Int63.glob
 src/versions/standard/Int63/Int63.v
-src/versions/standard/Int63/Int63.v.d
-src/versions/standard/Int63/Int63.vo
-src/versions/standard/Int63/Int63Axioms.glob
 src/versions/standard/Int63/Int63Axioms.v
-src/versions/standard/Int63/Int63Axioms.v.d
-src/versions/standard/Int63/Int63Axioms.vo
-src/versions/standard/Int63/Int63Native.glob
 src/versions/standard/Int63/Int63Native.v
-src/versions/standard/Int63/Int63Native.v.d
-src/versions/standard/Int63/Int63Native.vo
-src/versions/standard/Int63/Int63Op.glob
 src/versions/standard/Int63/Int63Op.v
-src/versions/standard/Int63/Int63Op.v.d
-src/versions/standard/Int63/Int63Op.vo
-src/versions/standard/Int63/Int63Properties.glob
 src/versions/standard/Int63/Int63Properties.v
-src/versions/standard/Int63/Int63Properties.v.d
-src/versions/standard/Int63/Int63Properties.vo
-src/versions/standard/Structures.glob
 src/versions/standard/Structures.v
-src/versions/standard/Structures.v.d
-src/versions/standard/Structures.vo
-src/versions/standard/structures.cmi
-src/versions/standard/structures.cmo
-src/versions/standard/structures.cmx
-src/versions/standard/structures.ml.d
-src/versions/standard/structures.mli.d
-src/versions/standard/structures.o
-src/zchaff/cnfParser.cmo
-src/zchaff/satParser.cmo
-src/zchaff/zchaff.cmo
-src/zchaff/zchaffParser.cmo