aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
Commit message (Expand)AuthorAge
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* Modification of the Scheme command.Gravatar vsiles2007-09-28
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...Gravatar herbelin2007-08-24
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)Gravatar herbelin2007-02-24
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
* Petit oubli dans commit 9474Gravatar herbelin2007-01-11
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* making otags working Gravatar jforest2006-08-22
* Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...Gravatar herbelin2006-07-05
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26