diff options
Diffstat (limited to 'contrib/omega/coq_omega.ml')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index ee3301d7..da0817d1 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id: coq_omega.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: coq_omega.ml 8934 2006-06-09 14:30:12Z herbelin $ *) open Util open Pp @@ -162,10 +162,12 @@ let hide_constr,find_constr,clear_tables,dump_tables = open Coqlib let logic_dir = ["Coq";"Logic";"Decidable"] +let init_arith_modules = init_modules @ arith_modules let coq_modules = - init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + init_arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] +let init_arith_constant = gen_constant_in_modules "Omega" init_arith_modules let constant = gen_constant_in_modules "Omega" coq_modules (* Zarith *) @@ -268,17 +270,17 @@ let coq_Zge = lazy (constant "Zge") let coq_Zlt = lazy (constant "Zlt") (* Peano/Datatypes *) -let coq_le = lazy (constant "le") -let coq_lt = lazy (constant "lt") -let coq_ge = lazy (constant "ge") -let coq_gt = lazy (constant "gt") -let coq_minus = lazy (constant "minus") -let coq_plus = lazy (constant "plus") -let coq_mult = lazy (constant "mult") -let coq_pred = lazy (constant "pred") -let coq_nat = lazy (constant "nat") -let coq_S = lazy (constant "S") -let coq_O = lazy (constant "O") +let coq_le = lazy (init_arith_constant "le") +let coq_lt = lazy (init_arith_constant "lt") +let coq_ge = lazy (init_arith_constant "ge") +let coq_gt = lazy (init_arith_constant "gt") +let coq_minus = lazy (init_arith_constant "minus") +let coq_plus = lazy (init_arith_constant "plus") +let coq_mult = lazy (init_arith_constant "mult") +let coq_pred = lazy (init_arith_constant "pred") +let coq_nat = lazy (init_arith_constant "nat") +let coq_S = lazy (init_arith_constant "S") +let coq_O = lazy (init_arith_constant "O") (* Compare_dec/Peano_dec/Minus *) let coq_pred_of_minus = lazy (constant "pred_of_minus") |