aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-08-05Better fix of e5c025Pierre Boutillier
2014-08-04One more optimization for guard checking of cofixpoints.Maxime Dénès
2014-08-04More optimization in guard checking.Maxime Dénès
2014-08-04Fix an exponential behavior in guard checker for cofixpoints.Maxime Dénès
2014-08-04Fixing semantics of Univ.Level.equal.Pierre-Marie Pédrot
2014-08-04STM: when looking up in the cache catch Expired excCarst Tankink
2014-08-04STM: generate Feedback message for parsing errorsEnrico Tassi
2014-08-04STM: use a real priority queueEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-08-04Some comments in the interface of Proofview_monad.Arnaud Spiwack
2014-08-04Cleaning the new implementation of the tactic monad continued.Arnaud Spiwack
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-08-03Fix to make Coq compile, I think this should still be accepted.Matthieu Sozeau
2014-08-03Fix infer conv using the wrong universe conversion flexibility informationMatthieu Sozeau
2014-08-03- Fix handling of opaque polymorphic definitions which were turned transparent.Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-03- Fix has_undefined_evars not using its or_sorts argument anymore.Matthieu Sozeau
2014-08-03Chapter 4: Fixing ambiguity about whether the return predicate refersHugo Herbelin
2014-08-03Fixing #3483 (graceful failing with notations to non-constructors in "match").Hugo Herbelin
2014-08-02Better struture for Ltac internalization environments in Constrintern.Pierre-Marie Pédrot
2014-08-01Faster uconstr.Arnaud Spiwack
2014-08-01CHANGES: [>…].Arnaud Spiwack
2014-08-01Document [> … ].Arnaud Spiwack
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
2014-08-01Fix English spelling -> American spelling in doc.Arnaud Spiwack
2014-08-01CHANGES: [numgoals] and [guard].Arnaud Spiwack
2014-08-01Document [numgoals] and [guard].Arnaud Spiwack
2014-08-01Add [guard] tactic.Arnaud Spiwack
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-08-01Add primtive [num_goal] to Proofview.Arnaud Spiwack
2014-08-01Untyped terms in ltac: simplify [coerce_to_uconstr].Arnaud Spiwack
2014-08-01Remove spurious [1] in equality.ml.Arnaud Spiwack
2014-08-01Clean outdated comment in Proofview.Notations.Arnaud Spiwack
2014-08-01Fix typo in cf04daec997.Arnaud Spiwack
2014-08-01micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Frédéric Besson
2014-08-01Compatibility for compilation with ocaml 3.12 (at least).Hugo Herbelin
2014-08-01micromega : improve efficiency/termination of type-checkingFrédéric Besson
2014-08-01Continuing (incomplete) cleaning of Inductiveops.Hugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-08-01Removing more tactic compatibility layer.Pierre-Marie Pédrot
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-07-31Useless export of Instance.eqeq. We hashcons everything before calling thisPierre-Marie Pédrot
2014-07-31Making the error message about bullets more precise.Pierre Courtieu
2014-07-31Removing the call to Weak.get_copy in hashsets.Pierre-Marie Pédrot
2014-07-31micromega : refification recognises @eq T for T convertible with Z or RFrédéric Besson
2014-07-31Typos.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:51:27 +0000