aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extract_env.ml
AgeCommit message (Expand)Author
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-08Updating headers.herbelin
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-05Dump references in Extractionpboutill
2012-06-01More cleaningppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-02Noise for nothingpboutill
2011-07-29Extract_env: generic = on prec_declaration replaced by prec_declaration_equalpuech
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
2011-05-05Extraction: allow extraction foo when foo is an alias notationletouzey
2011-04-15Extraction: nicer error when a toplevel module has no body (#2525)letouzey
2011-04-13Extraction: opaque terms are not traversed anymore by defaultletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07A new command "Separate Extraction"letouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
2010-07-02Extraction: better support of modulesletouzey
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
2010-06-28Extraction: remove a useless matchletouzey
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 14:16:39 +0000