diff options
| -rw-r--r-- | contrib/omega/coq_omega.ml | 21 | ||||
| -rw-r--r-- | interp/coqlib.ml | 11 |
2 files changed, 7 insertions, 25 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 79497310eb..3f5b6b77ed 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 *) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 914717d394..b684036344 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -65,15 +65,10 @@ let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] +let narith_dir = ["Coq";"NArith"] + let zarith_dir = ["Coq";"ZArith"] -let zarith_base_modules = [ - zarith_dir@["fast_integer"]; - zarith_dir@["zarith_aux"]; - zarith_dir@["auxiliary"]; - zarith_dir@["ZArith_dec"]; - zarith_dir@["Zmisc"]; - zarith_dir@["Wf_Z"] -] +let zarith_base_modules = [narith_dir;zarith_dir] let init_dir = ["Coq";"Init"] let init_modules = [ |