| Commit message (Expand) | Author | Age |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Removing more tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
* | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
* | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | 2014-07-31 |
* | Fix discrimination net which was not recognizing primitive projections. | Matthieu Sozeau | 2014-07-30 |
* | Untyped terms in tactic: add the possibility to use a typed term inside an un... | Arnaud Spiwack | 2014-07-29 |
* | Untyped terms in tactic: function [type_term c] to give a typed version of [c]. | Arnaud Spiwack | 2014-07-29 |
* | Add a type of untyped term to Ltac's value. | Arnaud Spiwack | 2014-07-29 |
* | Clean up obsolete comment. | Arnaud Spiwack | 2014-07-29 |
* | CPS-style tactic matching. We use the tactic monad as the target of the CPS. | Pierre-Marie Pédrot | 2014-07-28 |
* | Code cleaning in Tacenv. | Pierre-Marie Pédrot | 2014-07-27 |
* | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot | 2014-07-27 |
* | Removing dead code relative to or_metaid. | Pierre-Marie Pédrot | 2014-07-25 |
* | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack | 2014-07-25 |
* | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack | 2014-07-25 |
* | A slightly more fine grained way to check whether a TACTIC EXTEND is global o... | Arnaud Spiwack | 2014-07-25 |
* | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack | 2014-07-24 |
* | Small code sharing in TacticMatching. | Pierre-Marie Pédrot | 2014-07-22 |
* | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau | 2014-07-21 |
* | 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 |