diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc4698..7b52a9cee6 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -509,7 +509,7 @@ let coq_eqdec ~sum ~rev = let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in let args = [eqn; mkGAppRef coq_not_ref [eqn]] in let args = if rev then List.rev args else args in - mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]]) + mkPattern (mkGAppRef sum args) ) (** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *) |