| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-11-28 | Extraction: Richer patterns in matchs as proposed by P.N. Tollitte | letouzey |
| 2011-11-24 | Fixed some missing options from previous commit. | ppedrot |
| 2011-11-24 | Added a DEPRECATED flag in declaration of options. For now only two options a... | ppedrot |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-11-17 | Fixing bug #2640 and variants of it (inconsistency between when and | herbelin |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-11-14 | Bug 2636 - Move string_of_ppcmds to Pp | pboutill |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-10-28 | Remove dynamic stuff from constr_expr and glob_constr | glondu |
| 2011-10-27 | Remove avoidable use of GDynamic | glondu |
| 2011-10-22 | Fixing Equality.injectable which did not detect an equality without | herbelin |
| 2011-10-18 | Fix bug #2227 | msozeau |
| 2011-10-18 | Fix inductive coercion code in Program (bug #2378) | msozeau |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-10-07 | Fix bug #2557 and an issue with Propers for complement | msozeau |
| 2011-10-05 | Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612). | herbelin |
| 2011-09-27 | In Coq_config: get rid of coqsrc and make coqlib optional | glondu |
| 2011-09-26 | Added support for referring to subterms of the goal by pattern. | herbelin |
| 2011-09-26 | Generalizing subst_term_occ so that it supports an arbitrary matching | herbelin |
| 2011-09-23 | Fix commit 14489: missing Coq. in dirpath | letouzey |
| 2011-09-23 | Program: add some check_required_library (fix #2592) + some dead code removal | letouzey |
| 2011-09-16 | Omega: for non-arithmetical goals, try proving False from context (wish #2236) | letouzey |
| 2011-09-15 | Omega aware of Z.pred (fix #1912) | letouzey |
| 2011-09-09 | correction du bug 2047 | jforest |
| 2011-09-06 | Improved ltac code for zify (fix #2575). | letouzey |
| 2011-09-05 | Extraction Implicit: fix the numbering of constructor arguments | letouzey |
| 2011-09-02 | Bug 2589: Documentation patch of Hendrik Tews | pboutill |
| 2011-08-25 | Extraction: allow extraction of records with anonymous fields (fix #2555) | letouzey |
| 2011-08-08 | New proposition "rewrite Heq in H" for eq_rect (assuming that there is | herbelin |
| 2011-08-08 | Esubst: make types of substitutions & lifts private | puech |
| 2011-08-04 | moins de reification inutile, noatations standards | pottier |
| 2011-07-29 | Ring: replaced various generic = on constr by eq_constr, destructors etc. | puech |
| 2011-07-29 | Quote: replaced various generic = on constr by eq_constr, destructors etc. | puech |
