aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* MAJGravatar herbelin2000-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; ↵Gravatar herbelin2000-11-06
| | | | | | bah... + effet nettoyage Names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@808 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵Gravatar filliatr2000-11-06
| | | | | | constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau mode de compilation de .ml4Gravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus besoin de débrancher la preuve qui ne passait pasGravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus besoin de rajouter "Require Plus"Gravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour ne plus éviter temporairement le "Auto with zarith" !Gravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@802 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier ↵Gravatar herbelin2000-11-05
| | | | | | devenu tros gros pour la compilation en PowerPC git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement d'options avec ou sans argtsGravatar mohring2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Few OCaml files in contrib/xmlGravatar sacerdot2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@798 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation avec make de Solaris; README et INSTALLGravatar filliatr2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@797 85f007b7-540e-0410-9357-904b9bb8a0f7
* URI problem addressed, but not resolved yetGravatar sacerdot2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@796 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
| | | | | | | | car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
* .old virés (CVS est là pour ca)Gravatar filliatr2000-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un switch pour le debuggerGravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'Intuition (trop intelligent?)Gravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour eviter temporairement le "Auto with zarith"Gravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de Tauto et IntuitionGravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Priorite du Try/Orelse + Debug switch + correction bug dans PatternGravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour le Require Export (temporaire)Gravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajouts pour les tactiques utilisateurGravatar delahaye2000-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification message d'erreurGravatar herbelin2000-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@781 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage command -> constrGravatar herbelin2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simpl fait trop maintenant; faut adapterGravatar herbelin2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
* erreur dans intro_gen corrigéeGravatar filliatr2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chasse au Cast de CastGravatar herbelin2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementGravatar herbelin2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajoute : Ast dans la regle de grammaireGravatar mayero2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@774 85f007b7-540e-0410-9357-904b9bb8a0f7
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a jour TheoryListGravatar mohring2000-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@772 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseGravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ↵Gravatar herbelin2000-10-26
| | | | | | de l'instanciation des Meta dans plain_instance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Require Export recursifsGravatar filliatr2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Semi_Ring_Theory_of decommenteGravatar mohring2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retire les parentheses autour des tactiquesGravatar mohring2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'Gravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Simpl avec Cases cache sous plusieurs constantesGravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage var en named et decl en assumGravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@763 85f007b7-540e-0410-9357-904b9bb8a0f7
* ntrefiner.ml* removed in module xmlGravatar sacerdot2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Manquait le cas Constr de dyn_polynomGravatar herbelin2000-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug pop_path_prefix : List.rev manquantGravatar herbelin2000-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@760 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-10 02:51:09 +0000