From e6eef565639fb3840dd235eb675ece6e4dbeb082 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 16 Sep 2016 15:46:31 +0200 Subject: Addressing OCaml compilation warnings. One of them revealed a true bug. --- tactics/hipattern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/hipattern.ml') diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc469..7b52a9cee 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 } *) -- cgit v1.2.3