aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* 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
* mise a jourGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1031 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1019 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@964 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@948 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@937 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@931 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@914 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation calcul des implicites et declaration des constantes / inductifs / ↵Gravatar filliatr2000-11-21
| | | | | | variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@877 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@830 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 08:20:37 +0000