diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 19:27:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 19:27:26 +0000 |
| commit | 7b4ea9f501ad01f4c137aeeda06d8aef32c05b82 (patch) | |
| tree | fe5ce60725ece2cd9a00b7f97139ed044737d2c9 | |
| parent | 42db51f738d751b6feab165509eb3265c58049c6 (diff) | |
Verify Setoid is loaded before doing anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10774 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |