aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la compilation de coqc et coqmktop pour éviter le problème ↵Gravatar notin2006-05-26
| | | | | | de stripping automatique sous Fedora git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8865 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added contrib/funind to the path for ocamldebug-coqGravatar courtieu2006-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support des modules dans CoqdocGravatar notin2006-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
* removing a warningGravatar jforest2006-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation de Coqdoc au nouveau add_globGravatar notin2006-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite changement précédence by de assertGravatar herbelin2006-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8860 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8859 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ proprÃiété svn:ignore sur test-suiteGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8858 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour version 8852 de constrintern.mlGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8855 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 07:17:08 +0000