diff options
author | 2012-02-07 16:51:57 +0000 | |
---|---|---|
committer | 2012-02-07 16:51:57 +0000 | |
commit | 1a305fc0410e70fc36f59623d1f0e618f7ee9aab (patch) | |
tree | 0612b27ca05b00d84a84e2f492c83b320f517786 /CHANGES | |
parent | 8e30bdf78eb5feb274b16fb1db1c7350e771ee99 (diff) |
Documentation for Grab Existential Variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -12,6 +12,8 @@ Vernacular commands - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). +- New command "Grab Existential Variables" to transform the unresolved evars at + the end of a proof into goals. Tactics |