aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:38:06 +0200
committerThéo Zimmermann2019-05-22 17:38:06 +0200
commit049cfe725d334fb863df31ee9e03db4b54a64455 (patch)
tree2149121e604d2b369eb001289bf64adf508afc21 /doc/plugin_tutorial
parented7d118e8ee9a6725daafde31845981f5da8d2b4 (diff)
parent0001b6d108c2d2c058b0bfca7e0af888c026fe05 (diff)
Merge PR #10203: Fixing typos - Part 1
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: gares Reviewed-by: jfehrle Reviewed-by: vbgl
Diffstat (limited to 'doc/plugin_tutorial')
-rw-r--r--doc/plugin_tutorial/tuto3/src/g_tuto3.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
index 82ba45726e..f4d9e7fd5b 100644
--- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -33,7 +33,7 @@ TACTIC EXTEND collapse_hyps
END
(* More advanced examples, where automatic proof happens but
- no tactic is being called explicitely. The first one uses
+ no tactic is being called explicitly. The first one uses
type classes. *)
VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> { example_classes n }