aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Erreur commit constrintern.mlGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de précédence de l'argument du by de assert; ↵Gravatar herbelin2006-05-23
| | | | | | conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Error during last commit (coq didn't compile)Gravatar jforest2006-05-23
| | | | | | | Bug correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout substl_named_decl pour mode MapleGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)Gravatar jforest2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8848 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleanning code Gravatar jforest2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8847 85f007b7-540e-0410-9357-904b9bb8a0f7
* PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite des marquages de types et opacifications de lemmes dans les wrappers MakeGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a bug in identifiers manipulation Gravatar jforest2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8842 85f007b7-540e-0410-9357-904b9bb8a0f7
* LetTuple are now supported in FunctionGravatar jforest2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'appel à coqdoc (COQBIN)Gravatar notin2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8840 85f007b7-540e-0410-9357-904b9bb8a0f7
* encore un exemple ne marchant pas, ni avec omega ni avec romegaGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8839 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵Gravatar herbelin2006-05-22
| | | | | | bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8838 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵Gravatar herbelin2006-05-22
| | | | | | bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8837 85f007b7-540e-0410-9357-904b9bb8a0f7
* auto with zarith genere des sous-lemmes silencieusement, Gravatar letouzey2006-05-20
| | | | | | | | et ... <: ... with E:=Z_as_OT n'aime pas ca git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8836 85f007b7-540e-0410-9357-904b9bb8a0f7
* "subst." works now even when it exists an hypothesis have the form "x=x" in ↵Gravatar jforest2006-05-20
| | | | | | the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8835 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
| | | | | | | | | avec <: au lieu de : sans surprise de modules genre Raw partout ou autres alias dépliés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8834 85f007b7-540e-0410-9357-904b9bb8a0f7
* on cache autant que possible Raw dans FSet(Weak)List.MakeGravatar letouzey2006-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8833 85f007b7-540e-0410-9357-904b9bb8a0f7
* tests de RomegaGravatar letouzey2006-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8832 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de mes modifs recentesGravatar letouzey2006-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8830 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 ↵Gravatar letouzey2006-05-18
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendances pour List.vGravatar notin2006-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a bug in matching context on if. Gravatar jforest2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans List.vGravatar notin2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8826 85f007b7-540e-0410-9357-904b9bb8a0f7
* updating Function documentationGravatar jforest2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de [count_occ] dans List.vGravatar notin2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8824 85f007b7-540e-0410-9357-904b9bb8a0f7
* etoffage des notions de permutations (a la fois List.Permutation et ↵Gravatar letouzey2006-05-16
| | | | | | Permutation.permutation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans CREDITSGravatar notin2006-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8822 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de theories/FSets/DecidableTypeEx.vGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8821 85f007b7-540e-0410-9357-904b9bb8a0f7
* 3*rienGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8820 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'exemples de decidable typesGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8819 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit ajout concernant InAGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8818 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8817 85f007b7-540e-0410-9357-904b9bb8a0f7
* In_dec de nouveau transparentGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8816 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparartion d'un petit oubli cassant PrecedenceGraphGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8815 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar letouzey2006-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8814 85f007b7-540e-0410-9357-904b9bb8a0f7
* un Zgcd calculant dans coqGravatar letouzey2006-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2006-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction trou de typage des éliminations d'inductifs introduit dans ↵Gravatar herbelin2006-05-13
| | | | | | commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8810 85f007b7-540e-0410-9357-904b9bb8a0f7
* une fonction pouvant calculer le gcd en coqGravatar letouzey2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8809 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques ajouts venant des fichiers de Evelyne C. Gravatar letouzey2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8808 85f007b7-540e-0410-9357-904b9bb8a0f7
* decidabilite de InA Gravatar letouzey2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comments about profilingGravatar herbelin2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli des symboles du Latin-1Gravatar herbelin2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8805 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-20 12:08:49 +0000