summaryrefslogtreecommitdiff
path: root/plugins/firstorder/g_ground.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
-rw-r--r--plugins/firstorder/g_ground.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 9d3d8c99..29d41b81 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -85,7 +85,7 @@ let gen_ground_tac flag taco ids bases gl=
extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
let result=ground_tac solver startseq gl in
qflag:=backup;result
- with e ->qflag:=backup;raise e
+ with reraise ->qflag:=backup;raise reraise
(* special for compatibility with Intuition