| Age | Commit message (Expand) | Author |
|---|
| 2008-03-18 | Added a function to rebuild an elim scheme from elim_scheme_info. Will | courtieu |
| 2008-03-16 | Using the "relation" constant made some unifications fail in the new | msozeau |
| 2008-03-15 | Application de refresh_universes dans typing.ml et retyping.ml : les | herbelin |
| 2008-03-10 | Pas très propre de reposer sur la capture des anomalies (et cela | herbelin |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2008-02-13 | Essai de prise en compte de delta dans unify_0 (même sur termes non clos). | herbelin |
| 2008-02-01 | Unification de TacLetRecIn et TacLetIn. En particulier, on peut | herbelin |
| 2008-01-31 | Debug implementation of dependent induction/dependent destruction and documen... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-10-24 | Bugfix in abstract_generalize | msozeau |
| 2007-10-12 | Uniformisation du comportement de rewrite et rewrite in : quand le | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-08-07 | Add a new tactic to generalize an instantiated inductive predicate adding equ... | msozeau |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-05-28 | Retour à un message d'erreur d'apply qui montre un échec sans sans réduction | herbelin |
| 2007-05-23 | A fix for bug #1397: | letouzey |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-25 | New keyword "Inline" for Parameters and Axioms for automatic | soubiran |
| 2007-04-16 | Suite unification apply et eapply (l'un et l'autre profite maintenant | herbelin |
| 2007-04-15 | Essai de partage de code entre apply et eapply | herbelin |
| 2007-04-13 | Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant | herbelin |
| 2007-02-09 | Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu... | notin |
| 2007-02-06 | Report de la révision 9599 de la v8.1 dans le trunk | notin |
| 2006-12-26 | Report correction bug #1289 dans trunk (r9435 pour branche v8.1) | herbelin |
| 2006-12-13 | Dépliage du terme d'induction avant suppression quand celui-ci est un | herbelin |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-11-10 | Ajout de dépliage de l'énoncé, si besoin est, dans apply in | herbelin |
| 2006-10-26 | Petit bug apply in | herbelin |
| 2006-10-25 | Correction d'une tentative incorrecte (révision 9266) de clarification | herbelin |
| 2006-10-24 | Ajout de la tactique "apply in". | herbelin |
| 2006-10-23 | Fixed "Show intros" which did not look at hypothesis. | courtieu |
| 2006-10-03 | Changement de comportement du [rewrite ... in H]: Coq échoue si H | notin |
| 2006-09-01 | Correction bug d'ordonnancement des hyps d'induction dans induction/destruct | herbelin |
| 2006-07-28 | Reparation bug Show intros: les hypothèses introduites précédemment | courtieu |
| 2006-07-20 | Correction du bug #1116 | jforest |
| 2006-07-18 | amelioration du comportement de induction (retour a la version V8.0) | jforest |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-05-02 | Correction bug du correctif bug assert as | herbelin |
| 2006-05-02 | Bug assert as | herbelin |
| 2006-04-12 | induction on multiple arguments made better: | courtieu |
| 2006-04-11 | adding a new tactic [intro_avoiding idl] which acts as intro but prevents the | jforest |
| 2006-04-06 | Enlevement de message d'erreur garbage. | courtieu |
| 2006-04-05 | ajout d'un rattrapage d'erreur pour "induction using". | courtieu |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
