aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Fix test-suite 2255.vGravatar Pierre Boutillier2014-03-17
* Useless tactic bindings in Tacticals.Gravatar Pierre-Marie Pédrot2014-03-07
* Tentative fix for a very strange pervasive equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
* Fixing generic equality in Auto.Gravatar Pierre-Marie Pédrot2014-03-07
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
* Term dnets do no need to contain the afferent constr pattern in their nodes.Gravatar Pierre-Marie Pédrot2014-03-03
* Removing Termdn, and putting the relevant code in Btermdn. The current TermdnGravatar Pierre-Marie Pédrot2014-03-03
* Extruding code not depending of the functor argument in Termdn.Gravatar Pierre-Marie Pédrot2014-03-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 13:49:28 +0000