diff options
Diffstat (limited to 'tactics/eqdecide.ml4')
| -rw-r--r-- | tactics/eqdecide.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 5329029a8..89d2a85d8 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -73,7 +73,7 @@ let solveNoteqBranch side = (onLastHypId (fun id -> Extratactics.h_discrHyp id))) let h_solveNoteqBranch side = - Refiner.abstract_extended_tactic "solveNoteqBranch" [] + Refiner.abstract_extended_tactic (solveNoteqBranch side) (* Constructs the type {c1=c2}+{~c1=c2} *) |