| Age | Commit message (Expand) | Author |
|---|
| 2012-04-23 | Fix ocamlbuild compilation: remove subtac from *.itarget | letouzey |
| 2012-04-23 | correct abort in Function when a proof of inversion fails | letouzey |
| 2012-04-18 | Corrects a (very) longstanding bug of tactics. As is were, tactic expecting | aspiwack |
| 2012-04-17 | Remove the Dp plugin. | gmelquio |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-04-12 | remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commit | letouzey |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2012-03-26 | Module names and constant/inductive names are now in two separate namespaces | letouzey |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2012-03-18 | Fixing bug #2732 (anomaly when using the tolerance for writing | herbelin |
| 2012-03-14 | Fix merge. | msozeau |
| 2012-03-14 | Revise API of understand_ltac to be parameterized by a flag for resolution of... | msozeau |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-14 | Integrated obligations/eterm and program well-founded fixpoint building to to... | msozeau |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-14 | Remove support for "abstract typing constraints" that requires unicity of sol... | msozeau |
| 2012-03-02 | Glob_term.predicate_pattern: No number of parameters with letins. | pboutill |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-03-01 | New version of recdef : | jforest |
| 2012-03-01 | various corrections in invfun due to a modification in induction | jforest |
| 2012-02-29 | correcting a little bug in invfun.ml | jforest |
| 2012-02-29 | correction of bug 2457 | jforest |
| 2012-02-29 | In the syntax of pattern matching, "in" clauses are patterns. | pboutill |
| 2012-02-20 | Correct application of head reduction. | msozeau |
| 2012-02-15 | Avoid retrying uncessarily to prove independent remaining obligations in Prog... | msozeau |
| 2012-02-15 | Avoid unnecessary normalizations w.r.t. evars in Program. | msozeau |
| 2012-02-14 | - Fix dependency computation in eterm to not consider filtered variables. | msozeau |
| 2012-02-03 | correcting inversion in list of generated tcc of Function | letouzey |
| 2012-01-31 | Fix camlp4 compilation | pboutill |
| 2012-01-30 | Added an pattern / occurence syntax for vm_compute. | ppedrot |
| 2012-01-23 | Fix for Program Instance not separately checking the resolution of evars of t... | msozeau |
| 2012-01-23 | Another quick hack that works this time, to handle printing of locality in Pr... | ppedrot |
| 2012-01-20 | Reverted previous commit, which broke library compilation. | ppedrot |
| 2012-01-20 | This is a quick hack to permit the parsing of the locality flag in the Progra... | ppedrot |
| 2012-01-17 | Fixed the pretty-printing of the Program plugin. | ppedrot |
| 2012-01-14 | coq_micromega.ml: fix order of recursive calls to rconstant | glondu |
| 2012-01-14 | More newlines in debugging output of psatzl | glondu |
| 2012-01-13 | Added a Btauto plugin, that solves boolean tautologies. | ppedrot |
| 2012-01-12 | Fix typo | glondu |
| 2011-12-16 | Moving bullets (-, +, *) into stand-alone commands instead of being | courtieu |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-12-10 | Extraction: only do the test on generalizable lets for ocaml | letouzey |
| 2011-12-08 | Extraction: avoid internal eta-reduction (fix #2570) | letouzey |
| 2011-11-30 | Extraction: try to avoid issues with an Include directly inside a .v | letouzey |
| 2011-11-30 | Quick hack to avoid anomaly on using Program w/o having required JMeq. | herbelin |
| 2011-11-29 | Extraction: typo in last commit | letouzey |
| 2011-11-29 | fix for bug #2649 | corbinea |
