| Commit message (Expand) | Author | Age |
* | patch pour contourner l'échec de type_of_applied_inductive sur un inductif a... | herbelin | 2006-04-11 |
* | Fixes for new unification, not used in default version as it really changes u... | msozeau | 2006-04-10 |
* | + Changing a little functional schemes types | jforest | 2006-04-10 |
* | Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous... | msozeau | 2006-04-10 |
* | New unification can solve the problem without eta-expansion, | msozeau | 2006-04-10 |
* | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin | 2006-04-07 |
* | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
* | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey | 2006-04-06 |
* | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey | 2006-04-06 |
* | ouverture du bon scope (positive_scope) derriere le constructeur Npos de N | letouzey | 2006-04-06 |
* | Enlevement de message d'erreur garbage. | courtieu | 2006-04-06 |
* | resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses | letouzey | 2006-04-05 |
* | MAJ Licence FAQ | herbelin | 2006-04-05 |
* | on utilise explicitement Prop/iff pour certains morphismes pour eviter des wa... | letouzey | 2006-04-05 |
* | Suppression du test Proof with <tac> | notin | 2006-04-05 |
* | ajout d'un rattrapage d'erreur pour "induction using". | courtieu | 2006-04-05 |
* | Bug index addendum à cause mauvaise utilisation asection dans Helm.tex | herbelin | 2006-04-04 |
* | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin | 2006-04-02 |
* | Petite actualisation FAQ | herbelin | 2006-03-31 |
* | Amendement impression evar pour affichage des Meta par 'info' | herbelin | 2006-03-31 |
* | Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep | herbelin | 2006-03-30 |
* | Inductifs avec polymorphisme de sorte (version initiale) | herbelin | 2006-03-29 |
* | Ajout array_fold_map', list_fold_map' et list_remove_first | herbelin | 2006-03-29 |
* | pour coqdoc | letouzey | 2006-03-29 |
* | Nommage explicite de certains "intro" pour préserver la compatibilité | herbelin | 2006-03-28 |
* | - correction d'un bug dans coqdoc (multi_index) | notin | 2006-03-28 |
* | Correction bug/typo dans splay_prod_assum et ajout decomp_sort | herbelin | 2006-03-28 |
* | reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere... | letouzey | 2006-03-28 |
* | Correction d'un bug dans Coqdoc (indentation & mots clés) | notin | 2006-03-27 |
* | - correction du bug #1055 | notin | 2006-03-27 |
* | appel Zenon sans prelude | filliatr | 2006-03-27 |
* | r8709@thot: notin | 2006-03-25 01:48:46 +0100 | notin | 2006-03-25 |
* | r8708@thot: notin | 2006-03-24 18:55:01 +0100 | notin | 2006-03-25 |
* | r8686@thot: notin | 2006-03-20 19:29:09 +0100 | notin | 2006-03-25 |
* | utilisation de la VM pour la normalisation finale de romega | letouzey | 2006-03-24 |
* | Patch envoy\'e par Benjamin Gregoire, permettant de corriger | letouzey | 2006-03-24 |
* | on ignore TAGS au niveau svn | letouzey | 2006-03-23 |
* | correctifs de bug pour romega: | letouzey | 2006-03-23 |
* | Correction d'un bug sur 'make doc' et modification des propriétés dans doc/ | notin | 2006-03-23 |
* | Subtac fixes, single fixpoint definitions are working again. Added a toggle o... | msozeau | 2006-03-22 |
* | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau | 2006-03-22 |
* | - Correction bug calcul mind_consnrealargs, introduit à la révision | herbelin | 2006-03-22 |
* | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | herbelin | 2006-03-22 |
* | + destruct now works as induction on multiple arguments : | jforest | 2006-03-21 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8650 85f007b7-540e-04... | letouzey | 2006-03-21 |
* | Adding "New Functional Scheme" | jforest | 2006-03-20 |
* | Documentation | herbelin | 2006-03-18 |
* | MAJ documentation en syntaxe v8 | herbelin | 2006-03-18 |
* | Bug BYTEFLAGS pour compilation bin/parser | herbelin | 2006-03-18 |
* | Documentation mutual_inductive_body | herbelin | 2006-03-18 |