| Commit message (Expand) | Author | Age |
|---|
| * | Redo PMP's patch to rewriting to make it purely functional using state passing. |  Matthieu Sozeau | 2014-07-14 |
| * | Adding a "time" tactical for benchmarking purposes. In case the tactic |  Hugo Herbelin | 2014-07-13 |
| * | check_for_interrupt: better (but slower) in threading mode |  Enrico Tassi | 2014-07-10 |
| * | Fix a oversight in 5bf9e67b . |  Arnaud Spiwack | 2014-07-10 |
| * | Revert "time tac" (committed by mistake). | Hugo Herbelin | 2014-07-07 |
| * | time tac | Hugo Herbelin | 2014-07-07 |
| * | Using IStream coiterator to explicit the captured state of tactic matching re... |  Pierre-Marie Pédrot | 2014-07-05 |
| * | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau | 2014-07-03 |
| * | More efficient implementation of Ltac match, by inlining a stream map. | Pierre-Marie Pédrot | 2014-07-03 |
| * | In setoid_rewrite, force resolution of the contraints generated by rewriting ... | Matthieu Sozeau | 2014-07-02 |
| * | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin | 2014-07-01 |
| * | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | 2014-06-30 |
| * | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin | 2014-06-30 |
| * | Small refinement about whether it is tolerated for compatibility that | Hugo Herbelin | 2014-06-28 |
| * | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
| * | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | 2014-06-28 |
| * | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
| * | Add an init_setoid check in rewrite to avoid trying to get undefined references. |  Matthieu Sozeau | 2014-06-27 |
| * | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau | 2014-06-26 |
| * | Incorrect folding of evars in let_tac_gen made remember fail to store | Matthieu Sozeau | 2014-06-25 |
| * | In rewrite, wrong computation of the sort of the term to be rewritten in | Matthieu Sozeau | 2014-06-25 |
| * | In exact check, use e_type_of to ensure that universe constraints necessary | Matthieu Sozeau | 2014-06-25 |
| * | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau | 2014-06-24 |
| * | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | 2014-06-23 |
| * | Removing opens to Clenvtac to track its use more easily. | Pierre-Marie Pédrot | 2014-06-23 |
| * | Oops, I fixed the .ml's | Matthieu Sozeau | 2014-06-23 |
| * | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau | 2014-06-23 |
| * | Less goal-entering. | Pierre-Marie Pédrot | 2014-06-22 |
| * | Reindex section variables for typeclass resolution if their type changed. | Matthieu Sozeau | 2014-06-21 |
| * | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau | 2014-06-20 |
| * | Add an e_type_of to avoid losing universe constraints. | Matthieu Sozeau | 2014-06-20 |
| * | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | 2014-06-19 |
| * | - 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 |
| * | Improve hotspot in Auto. | Pierre-Marie Pédrot | 2014-06-17 |
| * | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | 2014-06-13 |
| * | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | 2014-06-12 |
| * | 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 |
| * | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | 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 |
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
| * | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin | 2014-06-06 |
| * | Fixes the lost evars when interpreting a change with pattern tactic. | Arnaud Spiwack | 2014-06-06 |
| * | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | 2014-06-06 |
Matthieu Sozeau
Hugo Herbelin
Enrico Tassi
Arnaud Spiwack
Pierre-Marie Pédrot
Matthieu Sozeau