diff options
| -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 *) |