| Age | Commit message (Expand) | Author |
|---|
| 2006-04-26 | Prise en compte du Require multiple | herbelin |
| 2006-04-26 | suite du pont entre Bvector et N | letouzey |
| 2006-04-26 | Replacing "GenFixpoint" with "Function" and "mes" with "measure" | jforest |
| 2006-04-26 | Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la créat... | notin |
| 2006-04-25 | Un gros coup de lifting pour IntMap: | letouzey |
| 2006-04-25 | un lemme de double inclusion | letouzey |
| 2006-04-25 | Reverting nf_betaiotaevar_preserving_vm_cast | jforest |
| 2006-04-25 | Code mort (suite) | herbelin |
| 2006-04-25 | Suppression code mort | herbelin |
| 2006-04-24 | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin |
| 2006-04-24 | Changement anomaly en failwith dans out_name pour utilisation par map_succeed | herbelin |
| 2006-04-24 | Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr; | herbelin |
| 2006-04-24 | + Handling "if" and cast in GenFixpoint | jforest |
| 2006-04-20 | decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty) | letouzey |
| 2006-04-16 | Nouveau mécanisme pour les modules interactifs : les arguments de | herbelin |
| 2006-04-16 | Added code to support "Program Lemma/Example... etc" | msozeau |
| 2006-04-15 | Inversion de l'ordre de chargement des objets logiques et non logiques | herbelin |
| 2006-04-15 | Tests notations | herbelin |
| 2006-04-15 | Test synchronisation chargement objets non logiques | herbelin |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-04-14 | Pas fier | herbelin |
| 2006-04-14 | mise a jour credits | cpaulin |
| 2006-04-14 | Enleve les commentaires | cpaulin |
| 2006-04-14 | Test files for subtac. | msozeau |
| 2006-04-14 | Maj configure, README, etc... | notin |
| 2006-04-14 | Premier jet annonce 8.1 | herbelin |
| 2006-04-14 | MAJ 8.1 | herbelin |
| 2006-04-14 | replacing whd_betaiotaevar_preserving_vm_cast | jforest |
| 2006-04-13 | MAJ 8.1-APP | herbelin |
| 2006-04-13 | MAJ 8.1-APP | herbelin |
| 2006-04-12 | Changement de licence pour le Tutoriel de Coq | notin |
| 2006-04-12 | Simplifying the proof of principles | jforest |
| 2006-04-12 | induction on multiple arguments made better: | courtieu |
| 2006-04-11 | Modification of "Show Intros": it now shows letins too. | courtieu |
| 2006-04-11 | adding a new tactic [intro_avoiding idl] which acts as intro but prevents the | jforest |
| 2006-04-11 | ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release) | courtieu |
| 2006-04-11 | patch pour contourner l'échec de type_of_applied_inductive sur un inductif a... | herbelin |
| 2006-04-10 | 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-07 | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-04-06 | 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-05 | 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 |
