diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:56:28 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:56:28 +0200 |
| commit | 51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (patch) | |
| tree | 0ccc548e3322db7b07fbab40aa834b9ca1bf9446 /tactics/class_tactics.ml | |
| parent | 4d54945d8df4b9b3c0bca17f5bd4d391d7012c8f (diff) | |
| parent | 8dc130ed11373928f18adc16e552d650209de75f (diff) | |
Merge PR #868: Fix debug trace of typeclasses eauto.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6cc9d3d55..3fc2fc31b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1143,7 +1143,7 @@ module Search = struct let res = if j = 0 then tclUNIT () else tclDISPATCH - (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) + (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j')))) in let finish nestedshelf sigma = let filter ev = |