aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2006-08-28"Essai de remplacement de "ex P" par "exists x, P x" suite àherbelin
2006-08-24JMeq maintenant applicable sur Typeherbelin
2006-08-14comparison functions should be Defined not Qedletouzey
2006-07-17Renommage sqtr_lem_1 (bug 1189)notin
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...herbelin
2006-07-09Argument Scope de list déplacé dans List.vherbelin
2006-07-06Typoherbelin
2006-07-06Quelques Hint inutilesherbelin
2006-07-04MAJ du manuel de référencenotin
2006-06-26Ajout de Zgcd_spec (compat.)notin
2006-06-25nouvel algorithme pour Zgcd (plus rapide) + un Qcompareletouzey
2006-06-25repetition d'hypotheses dans well_founded_induction_type_2letouzey
2006-06-23Passage des graphes de Function dans Type jforest
2006-06-09Modification déf de exists! pour éviter une éta-expansion et pouvoir être...herbelin
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...herbelin
2006-06-06+ ameliorating the tactic "functional induction"jforest
2006-06-05Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...letouzey
2006-06-04Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...herbelin
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
2006-05-31ajout de QArith dans les theories standardsletouzey
2006-05-31petits ajoutsletouzey
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
2006-05-30* suite de la revision des wrappers Makeletouzey
2006-05-29Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésherbelin
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-05-24Suite changement précédence by de assertherbelin
2006-05-23Changement de précédence de l'argument du by de assert; conséquences...herbelin
2006-05-22un debut de propriétés concernant FMapletouzey
2006-05-22suite des marquages de types et opacifications de lemmes dans les wrappers Makeletouzey
2006-05-22MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...herbelin
2006-05-22MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...herbelin
2006-05-20auto with zarith genere des sous-lemmes silencieusement, letouzey
2006-05-20suite tentative pour permettre l'utilisation de modules de FSetsletouzey
2006-05-19on cache autant que possible Raw dans FSet(Weak)List.Makeletouzey
2006-05-18git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...letouzey
2006-05-17Typo dans List.vnotin
2006-05-17Ajout de [count_occ] dans List.vnotin
2006-05-16etoffage des notions de permutations (a la fois List.Permutation et Permutati...letouzey
2006-05-153*rienletouzey
2006-05-15ajout d'exemples de decidable typesletouzey
2006-05-15petit ajout concernant InAletouzey
2006-05-14On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posletouzey
2006-05-14In_dec de nouveau transparentletouzey
2006-05-14reparartion d'un petit oubli cassant PrecedenceGraphletouzey
2006-05-13typoletouzey
2006-05-13un Zgcd calculant dans coqletouzey
2006-05-11une fonction pouvant calculer le gcd en coqletouzey
2006-05-11quelques ajouts venant des fichiers de Evelyne C. letouzey
2006-05-11decidabilite de InA letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 11:19:23 +0000