aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Collapse)AuthorAge
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
| | | | | | | | | | | la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug BYTEFLAGS pour compilation bin/parserGravatar herbelin2006-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8646 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
| | | | | | | | | | | | | pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8637@thot: notin | 2006-03-14 16:00:49 +0100Gravatar notin2006-03-14
| | | | | | | | | - intégration de doc dans le Makefile principal - correction d'une incompatibilité avec Tetex 3.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8623@thot: notin | 2006-03-08 12:40:57 +0100Gravatar notin2006-03-08
| | | | | | | Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8620@thot: notin | 2006-03-08 11:44:16 +0100Gravatar notin2006-03-08
| | | | | | | | | | | | | | Modifications diverses de Coqdoc: - modification du comportement par défaut de l'option --latex - ajout d'une option --stdout - réaménagement dans les sources (création de global.ml) - modification du parser de coqdoc pour regler les problèmes liés à  la syntaxe V8. - Correction du bug #1052 sur les commentaires en fin de ligne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularisation des preuves concernant la logique classique, ↵Gravatar herbelin2006-03-05
| | | | | | l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: sortie WhyGravatar filliatr2006-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add vernacular file for subtacGravatar coq2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a fileGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change in subtac modulesGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Julien:Gravatar bertot2006-02-08
| | | | | | | | | + Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment. + Bug correction in new functional induction + For now no induction principle for general recursive definition is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2006-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7983 85f007b7-540e-0410-9357-904b9bb8a0f7
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01
| | | | | | | | | | | | | | | | | Benjamin Gregoire, Gilles Barthe. For the moment, it is as followed: If one uses GenFixpoint instead of Fixpoint, then induction principles are generated on the fly (respecting the match structure written by the user, with wildcards etc). These principles can be used directly or by tactics "new functional induction" and "functional inversion". We will soon make "new functional induction" become "functional induction", before release of V8.1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de fichiers d'interprétation de la syntaxe primitive pour string et charGravatar herbelin2006-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7966 85f007b7-540e-0410-9357-904b9bb8a0f7
* dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoGravatar letouzey2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵Gravatar herbelin2006-01-04
| | | | | | (suite): correction des dépendances (et notamment non-dépendance en unix.cma) pour la création de printers.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction dépendance g_prim.ml4/q_coqast.ml4Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de -notop pour imposer l'absence de module toplevelGravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Débranchement des parseurs de syntaxe v7Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans ↵Gravatar herbelin2005-12-20
| | | | | | metasyntax.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7677 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug dans le make installGravatar narboux2005-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* commited new ringGravatar barras2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds tools to help in defining new general recursive functionsGravatar bertot2005-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7527 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -w y finalement pas admise par ocamlc <= 3.08.2Gravatar herbelin2005-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocaml 3.09Gravatar herbelin2005-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7514 85f007b7-540e-0410-9357-904b9bb8a0f7
* new congruenceGravatar corbinea2005-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7237 85f007b7-540e-0410-9357-904b9bb8a0f7
* reflexive tautoGravatar corbinea2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7233 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: ajout des prédicats de sortesGravatar coq2005-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7165 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: traitement des fixpointsGravatar coq2005-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot to remove a cmo.Gravatar coq2005-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added subtac contrib.Gravatar coq2005-05-25
| | | | | | | Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: ajout du prouveur ZenonGravatar coq2005-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interface vers outil de recherche WhelpGravatar herbelin2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* appel de Simplify depuis CoqGravatar coq2005-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de COQLIB/user-contrib à l'installation pour insister sur la ↵Gravatar herbelin2005-03-11
| | | | | | possibilité qu'il est utilisable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6824 85f007b7-540e-0410-9357-904b9bb8a0f7
* clean de parser.optGravatar herbelin2005-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving centralised discharge into dispatched discharge_function; required to ↵Gravatar herbelin2005-02-18
| | | | | | delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6683 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 07:04:40 +0000