aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fixing #3483 (graceful failing with notations to non-constructors in "match").Gravatar Hugo Herbelin2014-08-03
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* Faster uconstr.Gravatar Arnaud Spiwack2014-08-01
* CHANGES: [>…].Gravatar Arnaud Spiwack2014-08-01
* Document [> … ].Gravatar Arnaud Spiwack2014-08-01
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
* CHANGES: [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Add primtive [num_goal] to Proofview.Gravatar Arnaud Spiwack2014-08-01
* Untyped terms in ltac: simplify [coerce_to_uconstr].Gravatar Arnaud Spiwack2014-08-01
* Remove spurious [1] in equality.ml.Gravatar Arnaud Spiwack2014-08-01
* Clean outdated comment in Proofview.Notations.Gravatar Arnaud Spiwack2014-08-01
* Fix typo in cf04daec997.Gravatar Arnaud Spiwack2014-08-01
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
* Compatibility for compilation with ocaml 3.12 (at least).Gravatar Hugo Herbelin2014-08-01
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 02:31:02 +0000