aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* Made pretyping a functor over a coercion implementation. Pretyping.Default ↵Gravatar msozeau2006-03-22
| | | | | | | | | | | uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
* - 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
* 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
* 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
* majGravatar coq2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8138 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8116 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8101 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
* majGravatar coq2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8083 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8074 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8070 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8057 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8020 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8015 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
* majGravatar coq2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8007 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7989 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7981 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7975 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
* majGravatar coq2006-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7968 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7963 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7942 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7926 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7915 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7883 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
* majGravatar coq2006-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7857 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7824 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7814 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7792 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7770 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7753 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7745 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7741 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
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7736 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7730 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7690 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7678 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7663 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
* majGravatar coq2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7621 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7586 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7576 85f007b7-540e-0410-9357-904b9bb8a0f7
* A la demande de Julien ForestGravatar letouzey2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7573 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7541 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:12:54 +0000