| Commit message (Expand) | Author | Age |
* | Redo PMP's patch to rewriting to make it purely functional using state passing. | Matthieu Sozeau | 2014-07-14 |
* | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi | 2014-07-10 |
* | In setoid_rewrite, force resolution of the contraints generated by rewriting ... | Matthieu Sozeau | 2014-07-02 |
* | Add an init_setoid check in rewrite to avoid trying to get undefined references. | Matthieu Sozeau | 2014-06-27 |
* | In rewrite, wrong computation of the sort of the term to be rewritten in | Matthieu Sozeau | 2014-06-25 |
* | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau | 2014-06-23 |
* | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau | 2014-06-20 |
* | - Fix bug in unification, not only named metas are turned into evars (e.g. in... | Matthieu Sozeau | 2014-06-19 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau | 2014-06-11 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
* | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | 2014-06-08 |
* | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | 2014-06-08 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin | 2014-05-31 |
* | Removing a tclSENSITIVE from rewrite. | Pierre-Marie Pédrot | 2014-05-27 |
* | Update and start testing rewrite-in-type code. | Matthieu Sozeau | 2014-05-09 |
* | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | 2014-05-08 |
* | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | 2014-05-08 |
* | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
* | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau | 2014-05-06 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | 2014-03-05 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Get rid of the enterl/glist API for Proofview.Goal. | Arnaud Spiwack | 2014-02-27 |
* | Removing unused tactics in rewrite. | Pierre-Marie Pédrot | 2014-01-14 |
* | Code cleaning in Rewrite, may also result faster. | Pierre-Marie Pédrot | 2014-01-04 |
* | Qed: feedback when type checking is done | Enrico Tassi | 2013-12-24 |
* | Simplifying the use of hypinfos in Rewrite. | Pierre-Marie Pédrot | 2013-12-24 |
* | Rewrite.ml: removing direction flag from hypinfo. | Pierre-Marie Pédrot | 2013-12-23 |
* | Do not pass unification flags around in Rewrite. | Pierre-Marie Pédrot | 2013-12-22 |
* | Slight code cleaning ensuring more static invariants in Rewrite. | Pierre-Marie Pédrot | 2013-12-22 |
* | Dedicated inductive for return values of rewrite strategies. | Pierre-Marie Pédrot | 2013-12-16 |
* | Writing [cut] tactic using the new monad. | Pierre-Marie Pédrot | 2013-12-02 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Porting Tactics.assumption to the new engine. | ppedrot | 2013-11-08 |
* | Tachmach.New is now in Proofview.Goal.enter style. | aspiwack | 2013-11-02 |
* | More Proofview.Goal.enter. | aspiwack | 2013-11-02 |
* | The tactic [admit] exits with the "unsafe" status. | aspiwack | 2013-11-02 |
* | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack | 2013-11-02 |
* | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack | 2013-11-02 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Conv_orable made functional and part of pre_env | gareuselesinge | 2013-10-31 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | declaration_hooks use Ephemeron | gareuselesinge | 2013-10-18 |
* | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |