diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 48c94a074..8cf4d90a6 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1418,9 +1418,11 @@ let general_s_rewrite_in id l2r c ~new_goals gl = let hypinfo = ref (get_hyp gl c (Some id) l2r) in cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] (Some (([],id), [])) gl -let general_s_rewrite_clause = function - | None -> general_s_rewrite - | Some id -> general_s_rewrite_in id +let general_s_rewrite_clause x = + init_setoid (); + match x with + | None -> general_s_rewrite + | Some id -> general_s_rewrite_in id let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause |