aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-11-18Clarifying the role of ListSet.v in the library, compared to otherHugo Herbelin
2014-11-17Adding notation terminals to coqtop highlight.Pierre-Marie Pédrot
2014-11-17Fixing semantics of Ppconstr.print_hunks.Pierre-Marie Pédrot
2014-11-17Missing keywords in Ppconstr.Pierre-Marie Pédrot
2014-11-17Setting printing tags for Ltac.Pierre-Marie Pédrot
2014-11-17Moving printing code for red_expr and may_eval to Pptactic.Pierre-Marie Pédrot
2014-11-17Documenting the -color option.Pierre-Marie Pédrot
2014-11-17Documenting use of colors in Coq.Pierre-Marie Pédrot
2014-11-17Default styles for printing tags.Pierre-Marie Pédrot
2014-11-17Setting error tag on generic errors returned by Coqtop.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-25 04:00:47 +0000