diff options
author | 2003-11-04 13:59:11 +0000 | |
---|---|---|
committer | 2003-11-04 13:59:11 +0000 | |
commit | 96f08bc4901867065e76b05f8dfe74436bf00ad2 (patch) | |
tree | c48427ce094a0f4cbd5bf7dc6b8754f315eff1db /contrib/omega | |
parent | 2fb25aff118801d1a099ea5addeb17b8a3deec76 (diff) |
Extension de zarith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
-rw-r--r-- | contrib/omega/coq_omega.ml | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 79497310e..3f5b6b77e 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -143,25 +143,12 @@ let hide_constr,find_constr,clear_tables,dump_tables = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let init_dir = ["Coq";"Init"] -let arith_dir = ["Coq";"Arith"] -let logic_dir = ["Coq";"Logic"] -let zarith_dir = ["Coq";"ZArith"] -let coq_modules = [ - zarith_dir@["fast_integer"]; - zarith_dir@["zarith_aux"]; - zarith_dir@["auxiliary"]; - init_dir@["Datatypes"]; - init_dir@["Peano"]; - init_dir@["Logic"]; - arith_dir@["Compare_dec"]; - arith_dir@["Peano_dec"]; - arith_dir@["Minus"]; - logic_dir@["Decidable"] -] - open Coqlib +let logic_dir = ["Coq";"Logic";"Decidable"] +let coq_modules = + init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + let constant = gen_constant_in_modules "Omega" coq_modules (* Zarith *) |