aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Little reorganization of generalize tactics code w/o semantic changes.Gravatar Hugo Herbelin2014-05-08
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* Code cleaning in Tacinterp: factorizing some uses of tclEVARS.Gravatar Pierre-Marie Pédrot2014-05-08
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
* Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...Gravatar Matthieu Sozeau2014-05-06
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Avoid u+k <= v constraints, don't take the sup of an algebraic universe duringGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* Fixes after rebase. The use of pf_constr_of_global is problematic in presence...Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix abstract forgetting about new constraints.Gravatar Matthieu Sozeau2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Various fixes of universe polymorphism and projections when they're set.Gravatar Matthieu Sozeau2014-05-06
* Better hashconsing of levels and universes, working with modules.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Trying to improve the error messages of injection.Gravatar Maxime Dénès2014-04-30
* Injection: do not fail when arguments have sort Prop.Gravatar Maxime Dénès2014-04-29
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Giving true proof-terms in inversion instead of metas.Gravatar Pierre-Marie Pédrot2014-04-27
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Writing tclABSTRACT in the new monad. In particular the unsafe status is nowGravatar Pierre-Marie Pédrot2014-04-24
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing the compatibility layer from Leminv. Also removed an undocumentedGravatar Pierre-Marie Pédrot2014-04-22
* Using the new monad tactic in Inv.Gravatar Pierre-Marie Pédrot2014-04-22
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Small code cleaning in Tacticals.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Fixing bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
* Closing bug #3164Gravatar Julien Forest2014-04-04
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Removing dead code in Tactics.Gravatar Pierre-Marie Pédrot2014-03-31
* Using the new refine interface to define ML tactics.Gravatar Pierre-Marie Pédrot2014-03-28
* Define Tactics.bring_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-03-28
* Removing tactic compatibility layer from Eqdecide.Gravatar Pierre-Marie Pédrot2014-03-27
* Cosmetic changes in Equality.Gravatar Pierre-Marie Pédrot2014-03-27
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing tactic compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing tactic compatibility layer from Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Adding an interface to Eqdecide and putting the grammar rules in a dedicatedGravatar Pierre-Marie Pédrot2014-03-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-30 08:49:56 +0000