aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
* Typos.Gravatar Hugo Herbelin2014-07-31
* Finish fixes on notations and primitive projections, add test-suite files for...Gravatar Matthieu Sozeau2014-07-31
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
* Add test-suite file for bug #3439.Gravatar Matthieu Sozeau2014-07-30
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
* Fix discrimination net which was not recognizing primitive projections.Gravatar Matthieu Sozeau2014-07-30
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
* CHANGES: untyped terms in tacticsGravatar Arnaud Spiwack2014-07-29
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: add the possibility to use a typed term inside an un...Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
* Add test-suite file for bug 3454.Gravatar Matthieu Sozeau2014-07-29
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
* Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Gravatar Matthieu Sozeau2014-07-29
* Add test-suite file for bug #3453Gravatar Matthieu Sozeau2014-07-29
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
* Fix treatment of notations containing applications of projections (fixes bug ...Gravatar Matthieu Sozeau2014-07-29
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
* Pp: only one default feedback idGravatar Enrico Tassi2014-07-29
* Pp compiles after feedbackGravatar Enrico Tassi2014-07-29
* CPS-style tactic matching. We use the tactic monad as the target of the CPS.Gravatar Pierre-Marie Pédrot2014-07-28
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
* Code cleaning in Tacenv.Gravatar Pierre-Marie Pédrot2014-07-27
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
* CHANGES: cycle and swap.Gravatar Arnaud Spiwack2014-07-25
* Document swap tactic.Gravatar Arnaud Spiwack2014-07-25
* Document cycle tactic.Gravatar Arnaud Spiwack2014-07-25
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
* A slightly more fine grained way to check whether a TACTIC EXTEND is global o...Gravatar Arnaud Spiwack2014-07-25
* CHANGES: yellow in Coqide.Gravatar Arnaud Spiwack2014-07-25
* CHANGE: add Derive.Gravatar Arnaud Spiwack2014-07-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 02:36:19 +0000