| Age | Commit message (Expand) | Author |
|---|
| 2014-09-03 | Putting back normalized goals when entering them. | Pierre-Marie Pédrot |
| 2014-08-27 | Protect against "it's unifiable, if you solve some unsolvable constraints" be... | Matthieu Sozeau |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-08-21 | Removing a Goal.sensitive in Rewrite. | Pierre-Marie Pédrot |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot |
| 2014-08-21 | Removing a use of tclSENSITIVE in Rewrite. | Pierre-Marie Pédrot |
| 2014-08-18 | Improving error message when applying rewrite to an expression which is not a... | Hugo Herbelin |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-18 | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau |
| 2014-08-14 | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau |
| 2014-07-14 | Redo PMP's patch to rewriting to make it purely functional using state passing. | Matthieu Sozeau |
| 2014-07-10 | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi |
| 2014-07-02 | In setoid_rewrite, force resolution of the contraints generated by rewriting ... | Matthieu Sozeau |
| 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 |
