aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* ParsingGravatar herbelin2001-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVEGravatar herbelin2001-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Changement de place et de nom de la tactique Setoid_rewrite.Gravatar clrenard2001-07-10
| | | | | | | Maintenant On appelle Rewrite et il choisit si c'est un setoide ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a jour des .dependGravatar clrenard2001-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵Gravatar herbelin2001-06-25
| | | | | | définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵Gravatar herbelin2001-06-25
| | | | | | compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension des parametres de ClearGravatar delahaye2001-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des entrees puor Setoid_replace.Gravatar clrenard2001-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty -> PrettypGravatar filliatr2001-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place extraction haskellGravatar filliatr2001-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Rseries et Rtrigo_funGravatar mayero2001-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Fourier, DiscrR, ...Gravatar mayero2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1656 85f007b7-540e-0410-9357-904b9bb8a0f7
* remplace Zarith par ZArithGravatar mohring2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar courant2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de FieldGravatar delahaye2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding files for the production of textual explanations as used in pcoq.Gravatar bertot2001-04-18
| | | | | | | | | | dependence files are updated accordingly. Modifications in other files to cope with a few errors in the translation for the parser (mostly around records, coercions, and the search-pattern command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modified searchPattern. Before this correction, constructors were overlooked,Gravatar bertot2001-04-10
| | | | | | | | | | because the observation was done on the internal data-structure provided in the inductive definition. But this internal data-structure is not well-suited pattern-matching, since it contains debruijn indices where the inductive type should occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1572 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵Gravatar filliatr2001-04-04
| | | | | | d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the dependencies for the parser that is used in the interface pcoq.Gravatar bertot2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1546 85f007b7-540e-0410-9357-904b9bb8a0f7
* dependencies required for contrib/interfaceGravatar bertot2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1532 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1494 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1482 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction naive de fix et caseGravatar filliatr2001-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1447 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Explore générique et réécriture EAuto avec ce module; occur check ↵Gravatar filliatr2001-03-05
| | | | | | dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle implantation de la reductionGravatar barras2001-03-01
| | | | | | | suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stdlib -> Coqlib, Stock disparaitGravatar herbelin2001-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1382 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1345 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place extractionGravatar filliatr2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1339 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1338 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1334 85f007b7-540e-0410-9357-904b9bb8a0f7
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les Objdef introduisent une convertibilité avec les projections dans le ↵Gravatar herbelin2001-01-30
| | | | | | test de conversion de Evarconv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms longs dans les Hints et les Coercions, et ↵Gravatar herbelin2001-01-24
| | | | | | réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau module pour centraliser les chemins des constantes globales ↵Gravatar herbelin2001-01-19
| | | | | | utilisées dans le code de Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debut de reparation de simplGravatar mohring2000-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1083 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Portage d'AutoRewriteGravatar delahaye2000-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1043 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 16:24:40 +0000