diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 14 |
1 files changed, 14 insertions, 0 deletions
@@ -61,6 +61,20 @@ Coq binaries and process model `coq{proof,tactic,query}worker` are in charge of task-specific and parallel proof checking. +SSReflect + +- The implementation of delayed clear switches in intro patterns + is now simpler to explain: + 1. The immediate effect of a clear switch like {x} is to rename the + variable x to _x_ (i.e. a reserved identifier that cannot be mentioned + explicitly) + 2. The delayed effect of {x} is that _x_ is cleared at the end of the intro + pattern + 3. A clear switch immediately before a view application like {x}/v is + translated to /v{x}. + In particular rule 3 lets one write {x}/v even if v uses the variable x: + indeed the view is executed before the renaming. + Changes from 8.8.0 to 8.8.1 =========================== |