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