aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml
AgeCommit message (Expand)Author
2014-10-09Restoring plugins/xml/README erased by mistake.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-09-12Discontinued xml plugin: improve the README.Arnaud Spiwack
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-06-15- Fix xml plugin treatment of inductives.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-04Factoring(continued).Arnaud Spiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-14Remove some uses of local modules (some were unused, some were costly).xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-06still some more dead code removalletouzey
2012-10-06remove dumptree.ml4letouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-08-08Updating headers.herbelin
2012-06-01Cleaning Pp.ppnl useppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-02Noise for nothingpboutill
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:41:28 +0000