aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
2014-11-08Compatibility with 8.4 in the heuristic used to build the inductionHugo Herbelin
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-07Fixing Functional Induction when applied to an alias (reference manualHugo Herbelin
2014-11-07Granting #3717 (more informative error message on missing arguments for funct...Hugo Herbelin
2014-11-07Test for #3675 on primitive projections.Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
2014-11-07Test for #3542 fixed some time ago.Hugo Herbelin
2014-11-07doc: version number in cover.html + updates in coq.inria.fr stylePierre Letouzey
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-07Print [rename] tactic properly in info trace.Arnaud Spiwack
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-11-06Restoring clear_flag (thanks a lot to jonikelee to notice it).Hugo Herbelin
2014-11-06Optimizing when to clear generalized hypotheses in destruct.Hugo Herbelin
2014-11-06Dependency bug in using eqn for destruct.Hugo Herbelin
2014-11-06Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Hugo Herbelin
2014-11-06Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Hugo Herbelin
2014-11-06Removing "destruct" test not yet working.Hugo Herbelin
2014-11-06Fixing compilation (name of module Richprinter) I partially feelHugo Herbelin
2014-11-05lib/RichPp: Rename into Richpp.Yann Régis-Gianas
2014-11-05lib/richPp: Fix a bug related to the compatibility with ocaml 3.12Yann Régis-Gianas
2014-11-05printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Fix missing keyword tagging on definition introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Cosmetics.Yann Régis-Gianas
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-04ide/Xmlprotocol: Cosmetics.Yann Régis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04lib/richPp: Cosmetics.Regis-Gianas
2014-11-04printing/Ppannotation: New annotation for tactic syntactic objects.Regis-Gianas
2014-11-04printing/Pptactic.Make: New.Regis-Gianas
2014-11-04printing/Pptacticsig: New signature for tactic pretty-printers.Regis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04Rebase artefact.Regis-Gianas
2014-11-04lib/Pp.tag: New.Regis-Gianas
2014-11-04printing/Ppannotation: Introduce a new annotation for keywords.Regis-Gianas
2014-11-04printing/richPrinter: Fix incorrect signatures.Regis-Gianas
2014-11-04ide/Ide_slave.annotate: Implement annotate.Regis-Gianas
2014-11-04lib/Xml_parser.parse: Publish and document new interface.Regis-Gianas
2014-11-04lib/Xml_printer.pcdata_to_string: Publish.Regis-Gianas
2014-11-04printing/RichPrinter: New API for rich pretty-printing.Regis-Gianas
2014-11-04lib/Pp.rewrite: New.Regis-Gianas
2014-11-04lib/Xml_printer: Handle non-breakable spaces.Regis-Gianas
2014-11-04lib/Xml_parser.parse: Make canonicalization optional. (By default, it is appl...Regis-Gianas
2014-11-04lib/Xml_parser: Cosmetics.Regis-Gianas
2014-11-04lib/Xml_parser: Cosmetics.Regis-Gianas
2014-11-04Xml_lexer: Handle non-breakable spaces.Regis-Gianas
2014-11-04ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between i...Regis-Gianas
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:04:29 +0000