diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 18:59:11 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 18:59:11 +0100 |
| commit | 12a5ccdf1cb69c745aa72dad923349d411682f8d (patch) | |
| tree | 7636c3088a993c8381aa4fe6e485394ea91c0a87 /COMPATIBILITY | |
| parent | f5b7f689e6eeeb439346652566f6d841470376f4 (diff) | |
typo
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index f23dbad1c..ce5708093 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 |