aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-07-31Finish fixes on notations and primitive projections, add test-suite files for...Matthieu Sozeau
2014-07-31Consistent pretty-printing of primitive projections and their expanded forms.Matthieu Sozeau
2014-07-31Add an option to solve typeclass goals generated by apply which can't beMatthieu Sozeau
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-07-31Optimize check of new subterm relation on match.Maxime Dénès
2014-07-31Improve intersection of regular trees.Maxime Dénès
2014-07-31Fix dynamic computation of recargs for mutual inductives.Maxime Dénès
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-30Avoid hconsing instances during appends and conversions from/to arrays.Matthieu Sozeau
2014-07-30Fix discrimination net which was not recognizing primitive projections.Matthieu Sozeau
2014-07-30Avoid introducing additional universes when doing pruning in evarsolve.Matthieu Sozeau
2014-07-29CHANGES: untyped terms in tacticsArnaud Spiwack
2014-07-29Document untyped terms in tactics.Arnaud Spiwack
2014-07-29Small refactoring in Ltac parsing rules.Arnaud Spiwack
2014-07-29Allow [uconstr:c] as argument of a tactic.Arnaud Spiwack
2014-07-29Untyped terms in tactic: add the possibility to use a typed term inside an un...Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
2014-07-29Untyped term in tactics: add an grammar entry to construct them.Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-07-29Clean up obsolete comment.Arnaud Spiwack
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsMatthieu Sozeau
2014-07-29Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-29Fix bug #3453, not recognizing primitive projections in Coercion declarations.Matthieu Sozeau
2014-07-29Fix treatment of notations containing applications of projections (fixes bug ...Matthieu Sozeau
2014-07-29STM: print goals with no duplicatesEnrico Tassi
2014-07-29Pp: only one default feedback idEnrico Tassi
2014-07-29Pp compiles after feedbackEnrico Tassi
2014-07-28CPS-style tactic matching. We use the tactic monad as the target of the CPS.Pierre-Marie Pédrot
2014-07-28Adding a tclBREAK primitive to the tactic monad.Pierre-Marie Pédrot
2014-07-27Code cleaning in Tacenv.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-07-25Removing dead code relative to or_metaid.Pierre-Marie Pédrot
2014-07-25CHANGES: cycle and swap.Arnaud Spiwack
2014-07-25Document swap tactic.Arnaud Spiwack
2014-07-25Document cycle tactic.Arnaud Spiwack
2014-07-25Add a tactic [swap i j] to swap the position of goals [i] and [j].Arnaud Spiwack
2014-07-25Adds a cycle tactic to reorder goals in a loop.Arnaud Spiwack
2014-07-25A slightly more fine grained way to check whether a TACTIC EXTEND is global o...Arnaud Spiwack
2014-07-25CHANGES: yellow in Coqide.Arnaud Spiwack
2014-07-25CHANGE: add Derive.Arnaud Spiwack
2014-07-25CHANGE: document the features of the new tactic engine.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:53:37 +0000