aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-25Used an evar name based on the local def name in "evar" tactic.Hugo Herbelin
2014-11-25A bit more information in debug tactic unification.Hugo Herbelin
2014-11-25Adapting to current semantics of "simpl non-evaluable-cst"Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-24Plugging console highlighting in for toplevel and compilation error messages.Pierre-Marie Pédrot
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-24Fixing bug #3817.Pierre-Marie Pédrot
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-23Add printer for transparent state for ocamldebug.Hugo Herbelin
2014-11-23Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutHugo Herbelin
2014-11-23Fix #3824. de Bruijn error in normalization of fixpoints.Maxime Dénès
2014-11-22Specific printer of Evar.Set.t for ocamldebug + more information inHugo Herbelin
2014-11-22Attempt to organize and document unification flags of setoid rewrite.Hugo Herbelin
2014-11-22Removing superfluous newlines in setoid_rewrite error message.Hugo Herbelin
2014-11-22In setoid_rewrite error messages:Hugo Herbelin
2014-11-22Test for closed #2713 and #2876.Hugo Herbelin
2014-11-22Further simplifying functional induction.Hugo Herbelin
2014-11-22Simplifying code of functional induction.Hugo Herbelin
2014-11-22Not using an (arbitrary) pivot anymore for re-introduction ofHugo Herbelin
2014-11-22New simplification of code for generalizing hypotheses in destruct.Hugo Herbelin
2014-11-22Removing a hack which, according to the comment, should not be necessaryHugo Herbelin
2014-11-22Add test-suite file for dependent rewriting example by Vadim Zaliva andMatthieu Sozeau
2014-11-22Fix resolve_morphism to build well-scoped terms in case some argumentsMatthieu Sozeau
2014-11-22Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Pierre-Marie Pédrot
2014-11-22Writing intro_replacing in the new monad.Pierre-Marie Pédrot
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
2014-11-22Exporting a primitive allowing to run completely the tactic monad.Pierre-Marie Pédrot
2014-11-21Adding test for bug #3326.Pierre-Marie Pédrot
2014-11-21Adding test for bug #3424.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-21Test for bug #3788.Pierre-Marie Pédrot
2014-11-21Add test-suite file for bug #3804.Matthieu Sozeau
2014-11-21Fix bug #3804.Matthieu Sozeau
2014-11-21Avoid compilation warning.Matthieu Sozeau
2014-11-20Adding test for bug #3684.Pierre-Marie Pédrot
2014-11-20Fixing the previous commit. We had to normalize evars first.Pierre-Marie Pédrot
2014-11-20Somehow fixing a side-effect bug in tactics-in-terms.Pierre-Marie Pédrot
2014-11-20Probably useless use of a global-environment reading function in Indrec.Pierre-Marie Pédrot
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-11-20Re-removing the Hiddentac module. For some reason it had been reintroducedPierre-Marie Pédrot
2014-11-20Global.env chasing in Inv.Pierre-Marie Pédrot
2014-11-20Adding locations to tclZEROMSG.Pierre-Marie Pédrot
2014-11-20Setting printing flags on the printing of mutual inductives.Pierre-Marie Pédrot
2014-11-20Moving mutual inductive printing from Printer to Printmod.Pierre-Marie Pédrot
2014-11-19Making map_union a standard function of the ML library.Hugo Herbelin
2014-11-19Slightly improving error messages when mismatch with Proof using at Qed time.Hugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-19Continuing fixing nested but convertible occurrences in find_subtermHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:56:23 +0000