diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-16 07:41:03 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-16 07:41:03 -0400 |
| commit | eab9b0125238decef60a1710649671dc26959667 (patch) | |
| tree | e6f243721a2570c16b9aed66ffc5467950b92ad7 /CHANGES | |
| parent | 2c082f731f1fb6c867908504c4e454119e58e593 (diff) | |
Update CHANGES
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -21,6 +21,7 @@ Tactics - When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use a locally free identifier anymore. It must use e.g. the "fresh" primitive instead (potential source of incompatibilities). +- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO). Program |