aboutsummaryrefslogtreecommitdiff
path: root/pretyping/namegen.ml
AgeCommit message (Expand)Author
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-10-23Removing List.mem in Namegen. We may choose a better fitted datastructure tha...ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-02Noise for nothingpboutill
2012-01-27Printing bugs with match patterns:herbelin
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-09Commit 12485 continued.herbelin