aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
Commit message (Expand)AuthorAge
* Redo PMP's patch to rewriting to make it purely functional using state passing.Gravatar Matthieu Sozeau2014-07-14
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* In setoid_rewrite, force resolution of the contraints generated by rewriting ...Gravatar Matthieu Sozeau2014-07-02
* Add an init_setoid check in rewrite to avoid trying to get undefined references.Gravatar Matthieu Sozeau2014-06-27
* In rewrite, wrong computation of the sort of the term to be rewritten inGravatar Matthieu Sozeau2014-06-25
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Allow more relaxed conversion between the types of the two terms of a rewriteGravatar Matthieu Sozeau2014-06-20
* - Fix bug in unification, not only named metas are turned into evars (e.g. in...Gravatar Matthieu Sozeau2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix bug #3291, stack overflow in rewrite.Gravatar Matthieu Sozeau2014-06-11
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* Removing a tclSENSITIVE from rewrite.Gravatar Pierre-Marie Pédrot2014-05-27
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
* Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar 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
* 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
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
* Removing unused tactics in rewrite.Gravatar Pierre-Marie Pédrot2014-01-14
* Code cleaning in Rewrite, may also result faster.Gravatar Pierre-Marie Pédrot2014-01-04
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Simplifying the use of hypinfos in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-24
* Rewrite.ml: removing direction flag from hypinfo.Gravatar Pierre-Marie Pédrot2013-12-23
* Do not pass unification flags around in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
* Slight code cleaning ensuring more static invariants in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
* Dedicated inductive for return values of rewrite strategies.Gravatar Pierre-Marie Pédrot2013-12-16
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:45:48 +0000