aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
2003-04-10Affichage forcé des implicites contextuels si pas de contexte connuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3910 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Bug init_functionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Synchronisation séparée des implicites pour l'affichage du traducteur;herbelin
différentiation aussi pour les Implicites manuels; nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3893 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Correction Show Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3888 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Synchronisation avec resetherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3883 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Renommage unicite/unicity pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26ajout d'une fonction reset_modmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3791 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-13Ajout réaffichage SubClassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24False dependencies in summarycoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3695 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Ajout du traducteurdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03release 7.4; changement magic numberfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3652 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31Pour satisfaire ProofGeneralcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-27Deux p\'tits trucs ;)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3614 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Bug 'with Module' corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3573 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-16Petit netoyage des open's et commentairescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3448 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-11Essai de hconsing local au declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3422 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Hash-consing dès la lib_stkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3411 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Corrections de gestion des univers et modules + meilleure gestions des ↵coq
noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-05des Set et des Map en plusletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3379 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04Correction d'un message d'erreur de l'application de non-foncteurcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3375 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3351 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Quelques Set et Map spécialisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3335 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Affichage nom le plus court pour Syntactic Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3293 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout Refmapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3266 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Analyse plus fine des occurrences rigidesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3253 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-08Correction bug PR#222coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3224 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 15:35:37 +0000