aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
Commit message (Expand)AuthorAgeFilesLines
...
* Zeq_bool -> Z.eqbQuentin Garchery2018-10-271-4/+1
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-2/+2
* - auto-generated mli files for future documentationValentin Blot2017-11-247-0/+471
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-141-0/+3
* Compiles with both versions of CoqChantal Keller2017-10-032-4/+4
* Compiles with Coq-8.6Chantal Keller2017-10-033-11/+10
* Corrected a bug with holes in proofsChantal Keller2016-10-071-10/+9
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-10/+35
* Improved performance with coq-8.5Chantal Keller2016-09-281-13/+28
* More modularity on the format of traces depending on the version of coqChantal Keller2016-09-231-24/+24
* Now, Coq 8.5 is the defaultChantal Keller2016-05-011-59/+0
* Print warnings when checking proofs with holesChantal Keller2016-04-302-19/+31
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-8/+8
* Solved the efficiency problemChantal Keller2016-04-301-34/+83
* Holes in proof:Chantal Keller2016-04-304-13/+36
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-294-81/+113
* Updating of the copyrightChantal Keller2016-04-2712-22/+46
* The tactic "verit" generates more user-friendly subgoalsChantal Keller2016-04-262-13/+16
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-265-18/+34
* Compatibility with native-coqChantal Keller2016-04-262-11/+11
* Tactic verit for 8.5Chantal Keller2016-04-261-4/+4
* Tactic zchaff for 8.5Chantal Keller2016-04-261-7/+14
* Make the tactic available for 8.5Chantal Keller2016-04-261-8/+8
* Light port to Coq 8.5 under progressChantal Keller2016-03-184-69/+11
* Code refactoringChantal Keller2016-03-023-0/+273
* Removed old port to Coq 8.4Chantal Keller2016-03-021-0/+55
* Corrected a bug in the generation of certificates for CNF computation of iffChantal Keller2015-06-181-1/+1
* More on the support for standard Coq (not working yet)Chantal Keller2015-02-101-1/+1
* Identify ML functions that are implemented differently in native-coq and in s...Chantal Keller2015-01-132-3/+3
* Identify ML functions that depend on native-coqChantal Keller2015-01-136-22/+18
* Initial import of SMTCoq v1.2Chantal Keller2015-01-1211-0/+2755
generated by cgit (git 2.34.1) at 2024-06-29 09:29:03 +0000