diff options
| author | Yves Bertot | 2018-05-09 11:10:23 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-09 11:10:23 +0200 |
| commit | 499d48cba16ce5f42eff82e99cf8e0e08c796f8b (patch) | |
| tree | 1600222488ee5c3edc8d6324496a28b316ab7ef9 | |
| parent | c057f59599872b9ef98d5e2f4ffa9a7e5095916c (diff) | |
typo
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 index da14d03842..78deabed94 100644 --- a/tuto1/src/g_tuto1.ml4 +++ b/tuto1/src/g_tuto1.ml4 @@ -1,7 +1,7 @@ DECLARE PLUGIN "tuto1_plugin" (* If we forget this line and include our own tactic definition using - TACTIC EXTEND, as below, then we get the strage error message + TACTIC EXTEND, as below, then we get the strange error message no implementation available for Tacentries, only when compiling theories/Loader.v *) |