aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Port last changes of the guard condition to checker.Gravatar Maxime Dénès2014-08-06
* Relax a bit the guard condition.Gravatar Maxime Dénès2014-08-06
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
* Small code simplification.Gravatar Pierre-Marie Pédrot2014-08-05
* CoqIDE: fixing parsing of bullets and brackets even at end of file.Gravatar Hugo Herbelin2014-08-05
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
* Preliminary re-installation of notation interpretation in beautifying mode.Gravatar Hugo Herbelin2014-08-05
* Testing beautifying on an example.Gravatar Hugo Herbelin2014-08-05
* Fixing a few beautifying bugs.Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Chapter 4 of reference manual: Fixing asymmetric patterns error +Gravatar Hugo Herbelin2014-08-05
* Coqide: check_connection now also checks correct loading of coqide plugin +Gravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* Goal: API to get the solution of a goalGravatar Enrico Tassi2014-08-05
* make a few lines fit the screenGravatar Enrico Tassi2014-08-05
* STM: Classify Let as non asynchronous (Closes: #3486)Gravatar Enrico Tassi2014-08-05
* Coqide: annoying popups with GTK errors only in debug modeGravatar Enrico Tassi2014-08-05
* Ring: prevent an error message to show in case of success.Gravatar Arnaud Spiwack2014-08-05
* Documentation: a simple example for [numgoals].Gravatar Arnaud Spiwack2014-08-05
* Ltac's [idtac] is now interpreted outside of a goal if possible.Gravatar Arnaud Spiwack2014-08-05
* Ltac's idtac is now implemented using the new API.Gravatar Arnaud Spiwack2014-08-05
* Tacinterp: [interp_message] and associate now only require an environment rat...Gravatar Arnaud Spiwack2014-08-05
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
* Documentation of [uconstr]: typesetting.Gravatar Arnaud Spiwack2014-08-05
* Documentation: refine accept uconstr arguments.Gravatar Arnaud Spiwack2014-08-05
* Doc: uconstr now has a tactic notation entry.Gravatar Arnaud Spiwack2014-08-05
* Fix interpretation bug in [uconstr].Gravatar Arnaud Spiwack2014-08-05
* The [refine] tactic now accepts [uconstr].Gravatar Arnaud Spiwack2014-08-05
* Small refactoring: use [uconstr] instead of [constr] when relevant in grammar...Gravatar Arnaud Spiwack2014-08-05
* Properly declare uconstr as an argument for TACTIC EXTEND.Gravatar Arnaud Spiwack2014-08-05
* Fix [uconstr] name for argextend.Gravatar Arnaud Spiwack2014-08-05
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* One more optimization for guard checking of cofixpoints.Gravatar Maxime Dénès2014-08-04
* More optimization in guard checking.Gravatar Maxime Dénès2014-08-04
* Fix an exponential behavior in guard checker for cofixpoints.Gravatar Maxime Dénès2014-08-04
* Fixing semantics of Univ.Level.equal.Gravatar Pierre-Marie Pédrot2014-08-04
* STM: when looking up in the cache catch Expired excGravatar Carst Tankink2014-08-04
* STM: generate Feedback message for parsing errorsGravatar Enrico Tassi2014-08-04
* STM: use a real priority queueGravatar Enrico Tassi2014-08-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 15:16:27 +0000