aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3189 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Prise en compte let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3187 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-12Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3116 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-12Forcer la réouverture d'un fichier explicitement requis même si leherbelin
fichier a déjà été ouvert précédemment (peut-être indirectement) par un autre Require. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3115 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-10Nametab permet de definir le meme truc la deuxieme foiscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3111 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Nametab data structure reorganisationcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3030 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 07:25:33 +0000