| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | * | Update Coq84.v |  Jason Gross | 2016-01-12 | |
| | |_|/ |/| | | | | | | | | Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. | |||
| | | * | Move compatibility notations to their proper files |  Jason Gross | 2015-12-29 | |
| | |/ | ||||
| * | | Merge branch 'v8.5' |  Pierre-Marie Pédrot | 2015-12-15 | |
| |\| | ||||
| | * | Moved proof_admitted to its own file, named "AdmitAxiom.v". |  Maxime Dénès | 2015-12-14 | |
| | | | ||||
| * | | Updating Compat85.v after bd1c97653 on bracketing last or-and |  Hugo Herbelin | 2015-11-10 | |
| |/ | | | | introduction pattern by default. | |||
| * | Update compatibility file for some of bug #4392 | Jason Gross | 2015-11-03 | |
| | | | | | | | | | | | | | | 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' ``` | |||
| * | Add compatibility files (feature 4319) | Jason Gross | 2015-09-30 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |