aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixing bug #2279 (printing nested let-in was in exponential time)Gravatar herbelin2010-03-27
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Took local definitions into account in the test for deciding whetherGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Petite modif pour pouvoir faire "intros until 0" qui introduit autant Gravatar aspiwack2008-02-29
* Finish let| implementation and document itGravatar msozeau2008-01-31
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* 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
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
* Correction bug sur factorisation affichage paramètres (cf r9918)Gravatar herbelin2007-06-30
* Factorisation des types dans l'affichage des paramètres des (Co)Inductif/RecordGravatar herbelin2007-06-30
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Add functionality to permit printing terms with references to anonymous varia...Gravatar msozeau2007-02-16
* correction d'un bug d'efficacite dans le printerGravatar jforest2007-01-26
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar 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
* Version préliminaire d'inversion de la compilation du filtrageGravatar herbelin2006-01-16
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11