diff options
Diffstat (limited to 'plugins/omega/g_omega.ml4')
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index b2a5b5dc..46bbe2fd 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,14 +9,15 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) + +DECLARE PLUGIN "omega_plugin" open Coq_omega -open Refiner let omega_tactic l = let tacs = List.map @@ -25,12 +26,12 @@ let omega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No Omega knowledge base for type "^s)) - (Util.list_uniquize (List.sort compare l)) + | s -> Errors.error ("No Omega knowledge base for type "^s)) + (Util.List.sort_uniquize String.compare l) in - tclTHEN - (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) - omega_solver + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) + (omega_solver) TACTIC EXTEND omega @@ -39,7 +40,7 @@ END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.string_of_id l) ] + [ omega_tactic (List.map Names.Id.to_string l) ] | [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] END |