aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/xmlcommand.ml
Commit message (Expand)AuthorAge
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* - Fix xml plugin treatment of inductives.Gravatar Matthieu Sozeau2014-06-15
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* still some more dead code removalGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* plugins/xml: kill two warningsGravatar letouzey2010-06-03
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Fixing xml theory file export (was not consistent with coqdoc fileGravatar herbelin2009-11-26
* 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
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20