1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(**************************************************************************)
10
(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
12
(* Pierre Cr�gut (CNET, Lannion, France) *)
14
(**************************************************************************)
16
(*i camlp4deps: "parsing/grammar.cma" i*)
18
(* $Id: g_omega.ml4 10028 2007-07-18 22:38:06Z letouzey $ *)
26
| "nat" -> Tacinterp.interp <:tactic<zify_nat>>
27
| "positive" -> Tacinterp.interp <:tactic<zify_positive>>
28
| "N" -> Tacinterp.interp <:tactic<zify_N>>
29
| "Z" -> Tacinterp.interp <:tactic<zify_op>>
30
| s -> Util.error ("No Omega knowledge base for type "^s))
31
(Util.list_uniquize (List.sort compare l))
34
(tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
39
| [ "omega" ] -> [ omega_tactic [] ]
43
| [ "omega" "with" ne_ident_list(l) ] ->
44
[ omega_tactic (List.map Names.string_of_id l) ]
45
| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]