| Commit message (Expand) | Author | Age |
|---|
| * | global_reference migrated from Libnames to new Globnames, less deps in gramma... |  letouzey | 2012-05-29 |
| * | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey | 2012-05-29 |
| * | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey | 2012-05-29 |
| * | slim down a bit genarg.ml (pr_intro_pattern forgotten there) | letouzey | 2012-05-29 |
| * | Pattern as a mli-only file, operations in Patternops | letouzey | 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-05-29 |
| * | Fix ocamlbuild compilation: remove subtac from *.itarget | letouzey | 2012-04-23 |
| * | correct abort in Function when a proof of inversion fails | letouzey | 2012-04-23 |
| * | Corrects a (very) longstanding bug of tactics. As is were, tactic expecting |  aspiwack | 2012-04-18 |
| * | Remove the Dp plugin. |  gmelquio | 2012-04-17 |
| * | "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-04-12 |
| * | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey | 2012-03-30 |
| * | Module names and constant/inductive names are now in two separate namespaces | letouzey | 2012-03-26 |
| * | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey | 2012-03-23 |
| * | Fixing alpha-conversion bug #2723 introduced in r12485-12486. |  herbelin | 2012-03-20 |
| * | Fixing bug #2732 (anomaly when using the tolerance for writing | herbelin | 2012-03-18 |
| * | 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-14 |
| * | Glob_term.predicate_pattern: No number of parameters with letins. | pboutill | 2012-03-02 |
| * | Noise for nothing | pboutill | 2012-03-02 |
| * | New version of recdef : |  jforest | 2012-03-01 |
| * | various corrections in invfun due to a modification in induction | jforest | 2012-03-01 |
| * | 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-29 |
| * | Correct application of head reduction. | msozeau | 2012-02-20 |
| * | 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-15 |
| * | - Fix dependency computation in eterm to not consider filtered variables. | msozeau | 2012-02-14 |
| * | correcting inversion in list of generated tcc of Function | letouzey | 2012-02-03 |
| * | Fix camlp4 compilation | pboutill | 2012-01-31 |
| * | Added an pattern / occurence syntax for vm_compute. |  ppedrot | 2012-01-30 |
| * | 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-23 |
| * | 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-20 |
| * | Fixed the pretty-printing of the Program plugin. | ppedrot | 2012-01-17 |
letouzey
aspiwack
gmelquio
pboutill
herbelin
msozeau
jforest
ppedrot