From 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 00:20:30 +0100
Subject: Contradiction API using EConstr.

---
 ltac/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index bcfa13c79e..f87aa407d8 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -185,7 +185,7 @@ END
 open Contradiction
 
 TACTIC EXTEND absurd
- [ "absurd" constr(c) ] -> [ absurd c ]
+ [ "absurd" constr(c) ] -> [ absurd (EConstr.of_constr c) ]
 END
 
 let onSomeWithHoles tac = function
-- 
cgit v1.2.3