diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 2 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index d94a7136a..082eac422 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -26,7 +26,7 @@ let omega_tactic l = | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> | s -> Errors.error ("No Omega knowledge base for type "^s)) - (Util.List.uniquize (List.sort compare l)) + (Util.List.sort_uniquize String.compare l) in tclTHEN (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index a68196e8c..055546c8b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -19,7 +19,7 @@ let romega_tactic l = | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> | s -> Errors.error ("No ROmega knowledge base for type "^s)) - (Util.List.uniquize (List.sort compare l)) + (Util.List.sort_uniquize String.compare l) in tclTHEN (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) |