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