aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
Commit message (Expand)AuthorAge
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Removed obsolete v7->v8 translation code (function check_same_type isGravatar herbelin2010-04-29
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
* 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
* Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesGravatar herbelin2007-09-04
* Oubli dans commit 10102...Gravatar herbelin2007-08-30
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...Gravatar herbelin2007-08-24
* Factorisation des types dans l'affichage des paramètres des (Co)Inductif/RecordGravatar herbelin2007-06-30
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Ajout option Set Printing Universes et amélioration affichage des universGravatar herbelin2006-10-28
* Notations:Gravatar herbelin2006-10-09
* Déplacement surround dans util.ml et parenthésage des déclarationsGravatar herbelin2006-09-23
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19