aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Spotted a source of failure of the constr printer in debugger.Hugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-18Fix test-suite files.Matthieu Sozeau
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-18Fixing include of debugger.Pierre-Marie Pédrot
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-08-16Better printing of Ltac values.Pierre-Marie Pédrot
2014-08-16Fixing too restrictive detection of resolution of evars in "apply in"Hugo Herbelin
2014-08-15More self-contained code for tclWITHHOLES.Pierre-Marie Pédrot
2014-08-15Removing unused Refiner.tclWITHHOLES.Pierre-Marie Pédrot
2014-08-14Remove confusing behavior of unify_with_subterm that could fail withMatthieu Sozeau
2014-08-14Fix program using an the unsubstituted type of the original obligationMatthieu Sozeau
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-14Restore the error-handling behavior of [change], which was silently failingMatthieu Sozeau
2014-08-14Fix elimschemes accessing directly the universe context of inductives (fixes ...Matthieu Sozeau
2014-08-13Fix test-suite files according to new parsing rule for application of primitiveMatthieu Sozeau
2014-08-13Small optimization in Cooking: do not construct identity substitutions.Pierre-Marie Pédrot
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-12Upgrading output tests.Hugo Herbelin
2014-08-12Bug #3469: fixing unterminated comment.Hugo Herbelin
2014-08-12In bug #2406, renouncing to test failure of parsing error.Hugo Herbelin
2014-08-12Quick fix for avoiding infinitely many respawning and Warning "CoqHugo Herbelin
2014-08-12Fixing parsing of bullets after a "...".Hugo Herbelin
2014-08-12A couple of fixes/improvements in -beautify, but backtracking onHugo Herbelin
2014-08-10Fix bug introduced by earlier commit on first-order unification of primitiveMatthieu Sozeau
2014-08-09Fix unification which was failing when unifying a primitive projection againstMatthieu Sozeau
2014-08-09Allow pattern matching on the applied form of projections with primitiveMatthieu Sozeau
2014-08-09Do early occur-check in unification to allow eta to fire (fixes bug #3477)Matthieu Sozeau
2014-08-09Using the asymmetric merging primitive in Evd.Pierre-Marie Pédrot
2014-08-09Adding a primitive to merge ContextSets which is more efficient when onePierre-Marie Pédrot
2014-08-09Cleaning up interface of ContextSet.Pierre-Marie Pédrot
2014-08-09Tentative performance fix for Evd.merge_uctx.Pierre-Marie Pédrot
2014-08-08Change internalization of primitive projections to allow parsing [p t] asMatthieu Sozeau
2014-08-08Fix evarconv not applying eta when it used to. Fixes bug#3319.Matthieu Sozeau
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-07More .mailmap update.Arnaud Spiwack
2014-08-07Add some more entries to .mailmapArnaud Spiwack
2014-08-07Hypotheses in [Proofview.Goal.enter] were not normalised.Arnaud Spiwack
2014-08-07In Hipattern: some functions not working modulo evar instantiation.Arnaud Spiwack
2014-08-07Removing simple induction / destruct from the AST.Pierre-Marie Pédrot
2014-08-07Instead of relying on a trick to make the constructor tactic parse, putPierre-Marie Pédrot
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 19:02:52 +0000