| Commit message (Expand) | Author | Age |
... | |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
* | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
* | Death of "survive_module" and "survive_section" (the first one was | herbelin | 2009-08-13 |
* | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
* | - Add more precise error localisation when one of the application fails | herbelin | 2009-08-04 |
* | Added "etransitivity". | herbelin | 2009-08-03 |
* | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack | 2009-07-07 |
* | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau | 2009-06-30 |
* | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
* | - Added two new introduction patterns with the following temptative syntaxes: | herbelin | 2009-06-07 |
* | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin | 2009-05-10 |
* | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
* | - Fixed a little bug in previous commit (bad failure in case of unknown entry). | herbelin | 2009-04-27 |
* | - Cleaning (unification of ML names, removal of obsolete code, | herbelin | 2009-04-27 |
* | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin | 2009-04-24 |
* | nouvelle version de la tactique groebner proposee par Loic: | barras | 2009-04-16 |
* | Display the content of the list instead of "<list>" when an idtac | herbelin | 2009-04-05 |
* | Fix useless redeclaration of a tactic name when UpdateTac is replayed. | msozeau | 2009-03-28 |
* | Backport from v8.2 branch of 11986 (interpretation of quantified | herbelin | 2009-03-22 |
* | coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ... | barras | 2009-03-19 |
* | - gros commit sur ring et field: passage des arguments simplifie | barras | 2009-03-17 |
* | illegal tactic application was having Ltac interpreter loop | barras | 2009-03-04 |
* | commande Timeout + compaction des traces de debug_tactic | barras | 2009-03-04 |
* | Backtrack sur la mémoïsation de nf_evar. | aspiwack | 2009-03-04 |
* | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack | 2009-02-27 |
* | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
* | Fixed bugs #2001 (search_guard was overwriting the guard index given | herbelin | 2009-01-04 |
* | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin | 2009-01-02 |
* | - Added support for subterm matching in SearchAbout. | herbelin | 2008-12-29 |
* | About "apply in": | herbelin | 2008-12-09 |
* | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau | 2008-11-05 |
* | More debugging of handling of open constrs with typeclasses: | msozeau | 2008-10-25 |
* | Forgot one file which had other local modifications... | msozeau | 2008-10-23 |
* | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
* | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
* | Backporting 11445 from 8.2 to trunk (negative conditions in | herbelin | 2008-10-11 |
* | Correction de bugs: | herbelin | 2008-08-05 |
* | Évolutions diverses et variées. | herbelin | 2008-08-04 |
* | Propagation de l'information "strict" (càd à toplevel ou en train de | herbelin | 2008-07-24 |
* | Modification rapide du message d'erreur lorsqu'un _ ne peut être | herbelin | 2008-07-18 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | Quelques modifications autour du filtrage Ltac: | herbelin | 2008-07-16 |
* | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin | 2008-06-21 |
* | Little fixes: print unbound variable in error message (patch by Samuel | msozeau | 2008-06-19 |
* | incomplete bugfix for info | corbinea | 2008-06-19 |
* | Better typeclass error messages, always giving the full set of | msozeau | 2008-06-17 |
* | Add possibility to match on defined hypotheses, using brackets to | msozeau | 2008-06-16 |
* | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
* | - Correction de la version simplifiée (filtrage sur deux sig | herbelin | 2008-06-09 |