diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-25 10:16:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-25 10:16:57 +0200 |
| commit | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (patch) | |
| tree | 705a2b2de824b39d97a28fcea3b8287b53204b54 /plugins | |
| parent | 7d2dfd6fabd5d447166b1cb0e3b2993cc8abf4b3 (diff) | |
| parent | 069ab52e2af900d498395ebd1b00b7983152326e (diff) | |
Merge PR #6009: Master+misc typos dead code etc
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 |
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 } |