aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tactic_matching.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tactic_matching.ml')
-rw-r--r--plugins/ltac/tactic_matching.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 63b8cc482..18bb7d2db 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -203,7 +203,7 @@ module PatternMatching (E:StaticEnvironment) = struct
let pick l = pick l imatching_error
- (** Declares a subsitution, a context substitution and a term substitution. *)
+ (** Declares a substitution, a context substitution and a term substitution. *)
let put subst context terms : unit m =
let s = { subst ; context ; terms ; lhs = () } in
{ stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }