aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
Commit message (Expand)AuthorAge
* Restoring plugins/xml/README erased by mistake.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Discontinued xml plugin: improve the README.Gravatar Arnaud Spiwack2014-09-12
* 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
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* 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
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of nameGravatar ppedrot2012-12-18
* 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
* remove dumptree.ml4Gravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
* Updating headers.Gravatar herbelin2012-08-08
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Bug 2636 - Move string_of_ppcmds to PpGravatar pboutill2011-11-14
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27