aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7656 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de l'extraction haskell: affichage du type des fonctions, et ↵Gravatar letouzey2005-12-16
| | | | | | suppression des Sig git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7653 85f007b7-540e-0410-9357-904b9bb8a0f7
* multiples ameliorations de l'extraction scheme:Gravatar letouzey2005-12-16
| | | | | | | | | | - une syntaxe unique bigloo / pas bigloo (match sans ?) - un (load "macros_extr.scm") initial, et un mot sur ou le trouver - gestion des realisations d'axiomes - les ' dans les identifiateurs sont translates vers ~ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7651 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7648 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug dans le make installGravatar narboux2005-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7647 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7645 85f007b7-540e-0410-9357-904b9bb8a0f7
* changing the name of drgeocaml into GeoProofGravatar narboux2005-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7644 85f007b7-540e-0410-9357-904b9bb8a0f7
* More exception handling in functional scheme.Gravatar coq2005-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7643 85f007b7-540e-0410-9357-904b9bb8a0f7
* j'avais oublie ces deux fichiers.Gravatar gregoire2005-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7642 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug 881.Gravatar gregoire2005-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7641 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la generation des unsafeCoerceGravatar letouzey2005-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7632 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement parametres inductifs dans les theoriesGravatar mohring2005-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7
* evite certaines eta-expansions cavalieresGravatar letouzey2005-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7629 85f007b7-540e-0410-9357-904b9bb8a0f7
* correctif pour que type t = M.t contienne bien son M.Gravatar letouzey2005-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7627 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7626 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7622 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7621 85f007b7-540e-0410-9357-904b9bb8a0f7
* parametres inductifsGravatar mohring2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7620 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7618 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fonctionnalisation du cache 'compunit' pour réparer correctement le bug ↵Gravatar herbelin2005-11-26
| | | | | | #1030 (car add_frozen_state dans cache_require du commit précédent se faisait avant le add_leaf du require et cassait l'ordonnancement de la lib_stk pour le reset) + nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7615 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide send a ack to tell drgeocaml it is receivedGravatar narboux2005-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7614 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7611 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2005-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7609 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2005-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7608 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7606 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7604 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de coqide sous windows (bad file descriptor)Gravatar barras2005-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7599 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7596 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7593 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de la correction du test sur le nombre de parametres d'une projectionGravatar herbelin2005-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7590 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7587 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7586 85f007b7-540e-0410-9357-904b9bb8a0f7
* petites corrections + contournement bug projectionsGravatar barras2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7585 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7584 85f007b7-540e-0410-9357-904b9bb8a0f7
* commited new ringGravatar barras2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7583 85f007b7-540e-0410-9357-904b9bb8a0f7
* commited first version of new ringGravatar barras2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection de la version de lablgtk (type GText.view)Gravatar herbelin2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection de la version de lablgtk (type GText.view)Gravatar herbelin2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7580 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7577 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7576 85f007b7-540e-0410-9357-904b9bb8a0f7
* implement support for drgeocamlGravatar narboux2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7575 85f007b7-540e-0410-9357-904b9bb8a0f7
* merci les warnings de 3.09 ...Gravatar letouzey2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7574 85f007b7-540e-0410-9357-904b9bb8a0f7