aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssripats.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssripats.ml')
-rw-r--r--plugins/ssr/ssripats.ml2
1 files changed, 1 insertions, 1 deletions
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 =