| Commit message (Expand) | Author | Age |
... | |
* | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey | 2008-03-07 |
* | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
* | repair for commit 10612 (due to grammar order, some syntaxes weren't working) | letouzey | 2008-03-06 |
* | use loc instead of dummy_loc in the ugly intro-pattern rewrite hack | letouzey | 2008-03-04 |
* | Rework on rich forms of rewrite | letouzey | 2008-03-01 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
* | Suite ajout raccourcis à compute et lazy pour réduire tout sauf | herbelin | 2007-11-09 |
* | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
* | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin | 2007-09-30 |
* | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu | 2007-09-28 |
* | Generalized CAMLP4USE for pp dependencies | corbinea | 2007-07-16 |
* | More natural notation for intro pattern: @a -> ?a | glondu | 2007-07-09 |
* | Adding a syntax for "n-ary" rewrite: | letouzey | 2007-07-06 |
* | extension of the rename tactic: the following is now allowed: | letouzey | 2007-07-06 |
* | New intro pattern "@A", which generates a fresh name based on A. | glondu | 2007-07-06 |
* | Suggestion of additional syntax for intro patterns: | letouzey | 2007-07-06 |
* | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin | 2007-04-28 |
* | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
* | Mise en place d'un rafinement de compute. | jforest | 2007-04-05 |
* | Suppression de code mort | notin | 2007-02-01 |
* | Changement dans le kernel : | bgregoir | 2006-12-11 |
* | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
* | Changement de précédence de l'argument du by de assert; conséquences... | herbelin | 2006-05-23 |
* | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey | 2006-05-02 |
* | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
* | + destruct now works as induction on multiple arguments : | jforest | 2006-03-21 |
* | induction now admits multiple induction arguments. The principle must | coq | 2006-02-10 |
* | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin | 2006-01-28 |
* | Ajout de la contrainte que l'assertion doit être complètement prouvée dans... | herbelin | 2006-01-21 |
* | Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc... | herbelin | 2006-01-18 |
* | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq | herbelin | 2006-01-16 |
* | - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses | herbelin | 2006-01-16 |
* | cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets" | herbelin | 2006-01-16 |
* | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin | 2006-01-09 |
* | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin | 2005-12-26 |
* | Allow auto to have a parametric argument (wish #967) | herbelin | 2005-05-15 |
* | Added 'clear - id' to clear all hypotheses except the ones dependent in the s... | herbelin | 2005-03-07 |
* | Added 'clear - id' to clear all hypotheses except the ones dependent in the s... | herbelin | 2005-03-07 |
* | ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien... | herbelin | 2004-12-29 |
* | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin | 2004-12-09 |
* | Uniformisation du nom d'entrée openconstr en le nom du type open_constr | herbelin | 2004-12-06 |
* | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin | 2004-12-06 |
* | COMMITED BYTECODE COMPILER | barras | 2004-10-20 |
* | Suppression quotify | herbelin | 2004-07-16 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | moved instantiate binding to extratactics | corbinea | 2004-06-29 |
* | more evar stuff | corbinea | 2004-06-28 |
* | Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va... | herbelin | 2004-03-02 |
* | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin | 2004-03-01 |