aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
les contextes de preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2972 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Petites corrections ici et lacoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2746 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15MAJ V7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2689 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-16Déplacement/renommage de Class.stre_max en Declare.strength_minherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2648 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12Interdiction de nommer une constante comme une variable de section (plus ↵herbelin
simple que d'afficher en nom long...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2637 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22suppression de pop_namedbarras
meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Raffinement library_partherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2472 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Ajout library_partherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2467 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Correction de l'ordre des open (sachant que de toutes façons, unherbelin
Require au milieu d'un module sera considéré comme situé au début du module chargé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2432 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Pas d'assert false dans un try with !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2414 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Plusieurs arguments autorisés pour Require et Read Module; mise en place ↵herbelin
d'un mécanisme pour se souvenir de l'ordre des Open (mais pas activé); suppression du champ string dans le summary REQUIRE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2411 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-07Suppression de la dépendance des .vo en le nom physique des modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2379 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJ nombre magiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2335 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-17probleme des Require dans les sectionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2301 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05Rustine pour garder la compatibilité avec la 7.1 pour l'ordre des imports ↵herbelin
sans toutefois adopter l'ordre textuel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2266 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29reparation de Locatebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ↵herbelin
à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2200 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09Déplacement et export de type_of_global dans Globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2178 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Patch de goption.ml pour faire marcher les options synchrones. Passage des ↵letouzey
options d'extraction en synchrone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24One more boolean test bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2057 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24Bug test booléenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2056 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Réparation des options Set Printing and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Protection contre des arguments farfelus pour les implicites manuelsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2045 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21make docfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2041 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Nettoyage des commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2033 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Nettoyage des commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Nombre magique pour la V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2026 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:14:34 +0000