| Age | Commit message (Expand) | Author |
|---|
| 2014-06-27 | Add an init_setoid check in rewrite to avoid trying to get undefined references. | Matthieu Sozeau |
| 2014-06-25 | In rewrite, wrong computation of the sort of the term to be rewritten in | Matthieu Sozeau |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau |
| 2014-06-20 | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau |
| 2014-06-19 | - Fix bug in unification, not only named metas are turned into evars (e.g. in... | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-11 | 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-08 | 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-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-05-31 | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin |
| 2014-05-27 | Removing a tclSENSITIVE from rewrite. | Pierre-Marie Pédrot |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau |
| 2014-05-08 | 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-06 | - 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-03-05 | 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-02-27 | Get rid of the enterl/glist API for Proofview.Goal. | Arnaud Spiwack |
| 2014-01-14 | Removing unused tactics in rewrite. | Pierre-Marie Pédrot |
| 2014-01-04 | Code cleaning in Rewrite, may also result faster. | Pierre-Marie Pédrot |
| 2013-12-24 | 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-23 | Rewrite.ml: removing direction flag from hypinfo. | Pierre-Marie Pédrot |
| 2013-12-22 | 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-16 | Dedicated inductive for return values of rewrite strategies. | Pierre-Marie Pédrot |
| 2013-12-02 | Writing [cut] tactic using the new monad. | Pierre-Marie Pédrot |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-08 | Porting Tactics.assumption to the new engine. | ppedrot |
| 2013-11-02 | 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-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-18 | declaration_hooks use Ephemeron | gareuselesinge |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-10-05 | Fixing potential evar leak in Rewrite, and removing dead code. | ppedrot |
| 2013-09-28 | Made rewrite tactic strategies pure. They were using quite uglily | ppedrot |
| 2013-09-26 | Splitting Rewrite into a code part and a CAMLP4-dependent one. | ppedrot |
