| Age | Commit message (Expand) | Author |
|---|
| 2008-09-12 | Add a type argument to letin_tac instead of using casts and recomputing | msozeau |
| 2008-09-11 | Add enough information to correctly globalize recursive calls in inductive and | msozeau |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-18 | Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d... | notin |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-06-02 | Minor bug correction in recdef | jforest |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-04-28 | menage dans funind + deplaceemnt de recdef dans funind | jforest |
| 2008-04-25 | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin |
| 2008-04-24 | Remplacement de l'appel à interp_constr pour globaliser une constante | herbelin |
| 2008-04-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2008-04-12 | Désactivation du dumping des notations quand funind appelle les | herbelin |
| 2008-04-12 | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau |
| 2008-04-08 | correction of bug 1829 | jforest |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-18 | Added a function to rebuild an elim scheme from elim_scheme_info. Will | courtieu |
| 2008-03-15 | Adapt funind to the RLetPattern constructor. | msozeau |
| 2008-03-14 | Backtrack wrong commit. | courtieu |
| 2008-03-14 | indentation. | courtieu |
| 2008-03-13 | trying f | courtieu |
| 2008-03-08 | correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases) | jforest |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2008-01-09 | Correction of bug #1769 | jforest |
| 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-11-27 | bug correction in functional inversion principle generation | jforest |
| 2007-11-26 | minor bug correction in Function | jforest |
| 2007-11-19 | Bug in functionnal induction principle generation | jforest |
| 2007-11-08 | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin |
| 2007-10-30 | Cleaning code and comment. | courtieu |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-09-15 | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey |
| 2007-08-31 | correction bug d'efficacite dans Function | jforest |
| 2007-07-11 | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey |
| 2007-07-06 | extension of the rename tactic: the following is now allowed: | letouzey |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-05-17 | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-05 | Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func... | jforest |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-03-16 | r11153@tannat: jforest | 2007-03-16 10:25:55 +0100 | jforest |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-02-12 | Bug mineur dans la generation des principes d'induction pour Function | jforest |
