aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.mli
AgeCommit message (Expand)Author
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-07-16This is exactly the structure needed to handle controlling printingherbelin
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-02-16Add functionality to permit printing terms with references to anonymous varia...msozeau
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
2006-04-26- Utilisation d'abbréviations pour les types intervenant dans RCasesherbelin
2006-01-16Version préliminaire d'inversion de la compilation du filtrageherbelin
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-05-20Documentationherbelin
2005-01-03HUGE COMMITsacerdot
2004-07-16Nouvelle en-têteherbelin
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin