| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-05-29 | Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 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 |
