aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-09-10Un conv aurait dû être un conv_leqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1945 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Légère modification lookup_eliminatorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1943 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Amélioration check_module_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1939 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers ↵herbelin
algébriques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1937 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1936 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables ↵herbelin
de section au niveau du discharge, sans avoir à garder tout l'environnement de la section; suppression retypage du type des constantes déchargées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1935 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables ↵herbelin
de section au niveau du discharge, sans avoir à garder tout l'environnement de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Suppression du retypage dans w_Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1933 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1932 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Tests l'incohérence des universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1931 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-08MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1930 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1929 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1927 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-06Rétablissement de Print Sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1925 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-06Bug default module name (2eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1924 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-06Bug default module nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1923 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-05Version de la reduction dans Closure plus econome en memoire:barras
- la pile ne contient plus les arguments appliques deja consommes - ajout d'un "lock" sur les glacons en cours de calcul git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1922 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-04Nouveau coq.spec avec les droits de rootherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1921 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-03Correction d'un bug de pretty-print.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1919 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-31prise en compte de Load par coqdepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1918 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-30Fin de la modif Exc/optionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28Change la constante d'entree de Immediatemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1901 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28Remplace numarg -> pure_numarg dans Double Inductionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1900 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28remplace numarg -> pure_numargmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1899 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1898 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1897 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13bug de Bruijnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1896 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13bug incompatibilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1895 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Pour contourner un bug de camlp4 3.02herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1894 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Hack rapide pour réduire significativement la taille des voherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1893 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1892 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Prsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1891 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Prise en compte des strings et des flottants dans les statistiques de ↵herbelin
tailles mémoire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1890 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVEherbelin
Module : CONSTR/V7 Working dir: ~/V7uo/ In directory .: Modified .depend Modified CHANGES Unknown COMMIT Modified Makefile Modified TODO Unknown log.up Unknown parsing-sans-slam Unknown titi.v Unknown toto.v In directory contrib: Unknown contrib/interface_essai Unknown contrib/log In directory contrib/correctness: Modified contrib/correctness/pcic.ml Modified contrib/correctness/pmisc.ml Modified contrib/correctness/psyntax.ml4 In directory contrib/extraction: Modified contrib/extraction/extract_env.ml Modified contrib/extraction/haskell.ml Modified contrib/extraction/ocaml.ml Modified contrib/extraction/ocaml.mli In directory contrib/field: Modified contrib/field/field.ml4 Message: cvs server: New directory `contrib/interface' -- ignored Unknown contrib/interface/ctast.ml In directory contrib/omega: Modified contrib/omega/coq_omega.ml In directory contrib/ring: Modified contrib/ring/Setoid_ring_normalize.v Modified contrib/ring/quote.ml Modified contrib/ring/ring.ml Message: cvs server: New directory `contrib/setoid' -- ignored In directory contrib/xml: Modified contrib/xml/xmlcommand.ml In directory dev: Modified dev/base_include Modified dev/top_printers.ml In directory kernel: Modified kernel/cooking.ml Modified kernel/cooking.mli Modified kernel/environ.ml Modified kernel/environ.mli Unknown kernel/identifier.ml Unknown kernel/identifier.mli Modified kernel/names.ml Modified kernel/names.mli Modified kernel/safe_typing.mli Modified kernel/univ.ml In directory lib: Modified lib/system.ml Modified lib/system.mli Modified lib/util.ml Modified lib/util.mli In directory library: Modified library/declare.ml Modified library/declare.mli Modified library/global.ml Modified library/global.mli Modified library/lib.ml Modified library/lib.mli Modified library/library.ml Modified library/library.mli Modified library/nametab.ml Unknown library/nametab.ml.copie Unknown library/nametab.ml.saved Modified library/nametab.mli Unknown library/nametab.mli.saved In directory parsing: Modified parsing/ast.ml Modified parsing/ast.mli Modified parsing/astterm.ml Modified parsing/coqast.ml Modified parsing/coqast.mli Modified parsing/coqlib.ml Modified parsing/coqlib.mli Modified parsing/esyntax.ml Modified parsing/extend.ml4 Modified parsing/g_basevernac.ml4 Modified parsing/g_cases.ml4 Modified parsing/g_constr.ml4 Modified parsing/g_ltac.ml4 Modified parsing/g_prim.ml4 Modified parsing/g_rsyntax.ml Modified parsing/g_tactic.ml4 Modified parsing/g_vernac.ml4 Modified parsing/g_zsyntax.ml Modified parsing/lexer.ml4 Modified parsing/pcoq.ml4 Modified parsing/pcoq.mli Modified parsing/pretty.ml Modified parsing/prettyp.ml Modified parsing/printer.ml Modified parsing/q_coqast.ml4 Modified parsing/search.ml Modified parsing/termast.ml In directory pretyping: Modified pretyping/classops.ml Modified pretyping/syntax_def.ml In directory proofs: Modified proofs/proof_trees.ml Modified proofs/tacinterp.ml Modified proofs/tacinterp.mli In directory tactics: Modified tactics/Inv.v Modified tactics/dhyp.ml Modified tactics/inv.ml Modified tactics/inv.mli Modified tactics/setoid_replace.ml Modified tactics/tacticals.ml Modified tactics/tactics.ml Modified tactics/tauto.ml4 In directory test-suite: Unknown test-suite/vernac In directory theories: Message: cvs server: New directory `theories/Zarith' -- ignored In directory toplevel: Modified toplevel/class.ml Modified toplevel/command.ml Modified toplevel/command.mli Modified toplevel/coqinit.ml Modified toplevel/coqtop.ml Modified toplevel/discharge.ml Modified toplevel/discharge.mli Modified toplevel/mltop.ml4 Modified toplevel/record.ml Modified toplevel/vernacentries.ml Modified toplevel/vernacinterp.ml --------------------- End --------------------- -- last cmd: cvs -f -n update -d -P -- git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1888 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Renommage TrueCut -> Assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1886 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08La grammaire n'était plus LL1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1885 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Modification Tauto pour qu'il puisse destructurer des hypotheses de la formecourant
e1 -> e2 avec e1 type inductif ayant un unique constructeur constant. Cas typique : hypothese de la forme ~e=e. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1884 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵herbelin
tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-07Passage au nouveau Destructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1882 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 19:21:33 +0000