From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 plugins/ssr/ssripats.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 4a9dddd2b..7ae9e3824 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -95,7 +95,7 @@ let ssrmkabs id gl =
   end in
   Proofview.V82.of_tactic
     (Proofview.tclTHEN
-      (Tactics.New.refine step)
+      (Tactics.New.refine ~typecheck:false step)
       (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl
 
 let ssrmkabstac ids =
-- 
cgit v1.2.3