aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Replugging hints in rewriting strategies.Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3803.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing the unused boolean flag from the move tactic implementation.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Adding test for bug 3792.Gravatar Pierre-Marie Pédrot2014-11-09
* Fixing bug #3792.Gravatar Pierre-Marie Pédrot2014-11-09
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Gravatar Hugo Herbelin2014-11-08
* Continuing 3741c46fe134 on reporting ltac error.Gravatar Hugo Herbelin2014-11-08
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
* Test #3655 was failing due to an anomaly. Now it rather has to failGravatar Hugo Herbelin2014-11-08
* Test fixed by PMP's commits from Oct 21.Gravatar Hugo Herbelin2014-11-08
* Fixing doc of Functional Induction.Gravatar Hugo Herbelin2014-11-07
* Fixing Functional Induction when applied to an alias (reference manualGravatar Hugo Herbelin2014-11-07
* Granting #3717 (more informative error message on missing arguments for funct...Gravatar Hugo Herbelin2014-11-07
* Test for #3675 on primitive projections.Gravatar Hugo Herbelin2014-11-07
* Fixing #3562 ("as" in "destruct" expects either a disjunctiveGravatar Hugo Herbelin2014-11-07
* Test for #3542 fixed some time ago.Gravatar Hugo Herbelin2014-11-07
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Print [rename] tactic properly in info trace.Gravatar Arnaud Spiwack2014-11-07
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Dependency bug in using eqn for destruct.Gravatar Hugo Herbelin2014-11-06
* Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Gravatar Hugo Herbelin2014-11-06
* Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Gravatar Hugo Herbelin2014-11-06
* Removing "destruct" test not yet working.Gravatar Hugo Herbelin2014-11-06
* Fixing compilation (name of module Richprinter) I partially feelGravatar Hugo Herbelin2014-11-06
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
* lib/richPp: Fix a bug related to the compatibility with ocaml 3.12Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Fix missing keyword tagging on definition introducers.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Cosmetics.Gravatar Yann Régis-Gianas2014-11-05
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* ide/Xmlprotocol: Cosmetics.Gravatar Yann Régis-Gianas2014-11-04
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* lib/richPp: Cosmetics.Gravatar Regis-Gianas2014-11-04
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
* printing/Pptactic.Make: New.Gravatar Regis-Gianas2014-11-04
* printing/Pptacticsig: New signature for tactic pretty-printers.Gravatar Regis-Gianas2014-11-04
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* Rebase artefact.Gravatar Regis-Gianas2014-11-04
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
* printing/Ppannotation: Introduce a new annotation for keywords.Gravatar Regis-Gianas2014-11-04
* printing/richPrinter: Fix incorrect signatures.Gravatar Regis-Gianas2014-11-04
* ide/Ide_slave.annotate: Implement annotate.Gravatar Regis-Gianas2014-11-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 05:43:39 +0000