aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorJason Gross2015-10-30 13:32:42 -0400
committerPierre-Marie Pédrot2015-11-03 11:55:52 +0100
commit5f8f9e5b8eb22a413090229bc317fc2f36c053ac (patch)
tree291ddb2988a9ef20c811b0154f4dd51203703836 /kernel
parentdc65d720f3928fd987f82e1571521b52844dd248 (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