aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Some comments in the interface of Proofview_monad.Gravatar Arnaud Spiwack2014-08-04
* Cleaning the new implementation of the tactic monad continued.Gravatar Arnaud Spiwack2014-08-04
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* Fix to make Coq compile, I think this should still be accepted.Gravatar Matthieu Sozeau2014-08-03
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Fix has_undefined_evars not using its or_sorts argument anymore.Gravatar Matthieu Sozeau2014-08-03
* Chapter 4: Fixing ambiguity about whether the return predicate refersGravatar Hugo Herbelin2014-08-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 12:19:42 +0000