diff options
| author | Enrico Tassi | 2015-02-14 18:59:11 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-14 18:59:11 +0100 |
| commit | 12a5ccdf1cb69c745aa72dad923349d411682f8d (patch) | |
| tree | 7636c3088a993c8381aa4fe6e485394ea91c0a87 | |
| parent | f5b7f689e6eeeb439346652566f6d841470376f4 (diff) | |
typo
| -rw-r--r-- | COMPATIBILITY | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index f23dbad1c5..ce57080932 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -37,7 +37,7 @@ Tactic abstract. - Auxiliary lemmas generated by the abstract tactic are removed from the global environment and inlined in the proof term when a proof - is ended with Qed. The vehavior of 8.4 can be obtained by ending + is ended with Qed. The behavior of 8.4 can be obtained by ending proofs with "Qed export" or "Qed export ident, .., ident". Potential sources of incompatibilities between Coq V8.3 and V8.4 |