diff options
| author | Jason Gross | 2015-10-30 13:32:42 -0400 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-03 11:55:52 +0100 |
| commit | 5f8f9e5b8eb22a413090229bc317fc2f36c053ac (patch) | |
| tree | 291ddb2988a9ef20c811b0154f4dd51203703836 /kernel | |
| parent | dc65d720f3928fd987f82e1571521b52844dd248 (diff) | |
Update compatibility file for some of bug #4392
Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.
List obtained via
```
grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
