aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-08-06Port last changes of the guard condition to checker.Maxime Dénès
2014-08-06Relax a bit the guard condition.Maxime Dénès
2014-08-06Revert the change in Constrintern introduced by "Add a type of untyped term t...Arnaud Spiwack
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-06Removing "intros untils" from the AST.Pierre-Marie Pédrot
2014-08-05Adding a [make] primitive to the NonLogical monad.Pierre-Marie Pédrot
2014-08-05Small code simplification.Pierre-Marie Pédrot
2014-08-05CoqIDE: fixing parsing of bullets and brackets even at end of file.Hugo Herbelin
2014-08-05Uncountably many bullets (+,-,*,++,--,**,+++,...).Hugo Herbelin
2014-08-05Improving printing of "[]" (nil) in spite of the risk of collisionHugo Herbelin
2014-08-05Preliminary re-installation of notation interpretation in beautifying mode.Hugo Herbelin
2014-08-05Testing beautifying on an example.Hugo Herbelin
2014-08-05Fixing a few beautifying bugs.Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-08-05Making references to Proof General and CoqIDE uniform in Reference Manual.Hugo Herbelin
2014-08-05Chapter 4 of reference manual: Fixing asymmetric patterns error +Hugo Herbelin
2014-08-05Coqide: check_connection now also checks correct loading of coqide plugin +Hugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-05Goal: API to get the solution of a goalEnrico Tassi
2014-08-05make a few lines fit the screenEnrico Tassi
2014-08-05STM: Classify Let as non asynchronous (Closes: #3486)Enrico Tassi
2014-08-05Coqide: annoying popups with GTK errors only in debug modeEnrico Tassi
2014-08-05Ring: prevent an error message to show in case of success.Arnaud Spiwack
2014-08-05Documentation: a simple example for [numgoals].Arnaud Spiwack
2014-08-05Ltac's [idtac] is now interpreted outside of a goal if possible.Arnaud Spiwack
2014-08-05Ltac's idtac is now implemented using the new API.Arnaud Spiwack
2014-08-05Tacinterp: [interp_message] and associate now only require an environment rat...Arnaud Spiwack
2014-08-05Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Arnaud Spiwack
2014-08-05Documentation of [uconstr]: typesetting.Arnaud Spiwack
2014-08-05Documentation: refine accept uconstr arguments.Arnaud Spiwack
2014-08-05Doc: uconstr now has a tactic notation entry.Arnaud Spiwack
2014-08-05Fix interpretation bug in [uconstr].Arnaud Spiwack
2014-08-05The [refine] tactic now accepts [uconstr].Arnaud Spiwack
2014-08-05Small refactoring: use [uconstr] instead of [constr] when relevant in grammar...Arnaud Spiwack
2014-08-05Properly declare uconstr as an argument for TACTIC EXTEND.Arnaud Spiwack
2014-08-05Fix [uconstr] name for argextend.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 12:24:26 +0000