aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
Commit message (Collapse)AuthorAge
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3985 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3946 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3898 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour Reals/SeqSeries.vGravatar desmettr2003-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3680 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour renommage RcompletGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Binome.v -> Binomial.vGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3561 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3512 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage de TAF.v en MVT.vGravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage de RealsB en RbaseGravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3490 85f007b7-540e-0410-9357-904b9bb8a0f7
* bit vectorsGravatar filliatr2003-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3318 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Option pour compiler une version 'light' des réelsGravatar desmettr2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵Gravatar herbelin2002-11-24
| | | | | | améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj apres reparation d'un bug coqdepGravatar letouzey2002-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3244 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3241 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit du calcul des dependances un peu plus robusteGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3146 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep bogué, retour sur version 1.75Gravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3132 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵Gravatar herbelin2002-10-13
| | | | | | hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ClassicalFactsGravatar herbelin2002-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3113 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3102 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3093 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3070 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3062 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3038 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3022 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3021 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ depend.coqGravatar coq2002-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bugs TautoGravatar courant2002-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitGravatar courant2002-07-15
| | | | | | | de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2826 85f007b7-540e-0410-9357-904b9bb8a0f7
* resynchronisation du .depend.coqGravatar letouzey2002-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2810 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement contrib/correctness/ProgWf -> theories/ZArith/ZwfGravatar filliatr2002-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction vers schemeGravatar letouzey2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding file theories/ZArith/Zsqrt.v that contains a square root function.Gravatar bertot2002-06-07
| | | | | | | | | | | | | actually three functions are provided, one working on positive numbers (it is structurally recursive), one with a strong specification (Zsqrt), and one with a weak specification (Zsqrt_plain). For the function with a weak specification an extra theorem is also provided. The decision functions in ZArith_dec have been made transparent so that computation with the square root function also becomes possible with Lazy Beta Iota Delta Zeta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
* .depend.coq remis a jourGravatar letouzey2002-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2700 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2688 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-21 16:26:04 +0000