Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Moving the decompose tactic out of the AST. | 2014-09-01 | |
* | Lazy interpretation of patterns so that expressions such as "intros H H'/H" | 2014-08-18 | |
* | Adding a new intro-pattern for "apply in" on the fly. Using syntax | 2014-08-18 | |
* | Reorganisation of intropattern code | 2014-08-18 | |
* | [uconstr]: use a closure instead of eager substitution. | 2014-08-06 | |
* | Faster uconstr. | 2014-08-01 | |
* | Add a type of untyped term to Ltac's value. | 2014-07-29 | |
* | Moving wit_unit to Stdarg. | 2013-06-19 | |
* | Moving coercion functions out of Tacinterp. | 2013-06-12 |