aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-11-19Print [uconstr] in genargs.Arnaud Spiwack
2014-11-19Print [uconstr]-s in [idtac] messages.Arnaud Spiwack
2014-11-19Proper printer for [uconstr] in [Pptactic].Arnaud Spiwack
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-11-19Adding rich-printing facilities to Printmod.Pierre-Marie Pédrot
2014-11-18Tentative rephrasing of error message for rewrite.Hugo Herbelin
2014-11-18Hopefully the last word on having "simpl f" complying with theHugo Herbelin
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:33:12 +0000