diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 36 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 21 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 27 | ||||
| -rw-r--r-- | plugins/romega/const_omega.ml | 18 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 4 |
6 files changed, 58 insertions, 52 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 19a884323..53359e31d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -128,7 +128,7 @@ let def_of_const t = let coq_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ Coqlib.arith_modules) s;; + Coqlib.init_modules s;; let constant sl s = constr_of_global @@ -142,7 +142,7 @@ let find_reference sl s = (id_of_string s)));; let eq = lazy(coq_constant "eq") -let refl_equal = lazy(coq_constant "refl_equal") +let refl_equal = lazy(coq_constant "eq_refl") (*****************************************************************) (* Copy of the standart save mechanism but without the much too *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 92438db39..5499425df 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -236,6 +236,10 @@ let coq_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" (Coqlib.init_modules @ Coqlib.arith_modules) s;; +let coq_base_constant s = + Coqlib.gen_constant_in_modules "RecursiveDefinition" + (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; + let constant sl s = constr_of_global (locate (make_qualid(Names.make_dirpath @@ -250,23 +254,23 @@ let find_reference sl s = let delayed_force f = f () let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm") - -let le_trans = function () -> (coq_constant "le_trans") -let le_lt_trans = function () -> (coq_constant "le_lt_trans") -let lt_S_n = function () -> (coq_constant "lt_S_n") -let le_n = function () -> (coq_constant "le_n") -let refl_equal = function () -> (coq_constant "refl_equal") -let eq = function () -> (coq_constant "eq") -let ex = function () -> (coq_constant "ex") +let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm") + +let le_trans = function () -> (coq_base_constant "le_trans") +let le_lt_trans = function () -> (coq_base_constant "le_lt_trans") +let lt_S_n = function () -> (coq_base_constant "lt_S_n") +let le_n = function () -> (coq_base_constant "le_n") +let refl_equal = function () -> (coq_base_constant "eq_refl") +let eq = function () -> (coq_base_constant "eq") +let ex = function () -> (coq_base_constant "ex") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_sig = function () -> (coq_constant "sig") -let coq_O = function () -> (coq_constant "O") -let coq_S = function () -> (coq_constant "S") +let coq_sig = function () -> (coq_base_constant "sig") +let coq_O = function () -> (coq_base_constant "O") +let coq_S = function () -> (coq_base_constant "S") let gt_antirefl = function () -> (coq_constant "gt_irrefl") -let lt_n_O = function () -> (coq_constant "lt_n_O") -let lt_n_Sn = function () -> (coq_constant "lt_n_Sn") +let lt_n_O = function () -> (coq_base_constant "lt_n_O") +let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn") let f_equal = function () -> (coq_constant "f_equal") let well_founded_induction = function () -> (coq_constant "well_founded_induction") @@ -284,8 +288,8 @@ let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" (* These are specific to experiments in nat with lt as well_founded_relation, *) (* but this should be made more general. *) -let nat = function () -> (coq_constant "nat") -let lt = function () -> (coq_constant "lt") +let nat = function () -> (coq_base_constant "nat") +let lt = function () -> (coq_base_constant "lt") (* This is simply an implementation of the case_eq tactic. this code should be replaced with the tactic defined in Ltac in Init/Tactics.v *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cc667aa05..10cde3c56 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -136,22 +136,23 @@ struct ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] + let init_constant = gen_constant_in_modules "ZMicromega" init_modules let constant = gen_constant_in_modules "ZMicromega" coq_modules - let coq_and = lazy (constant "and") - let coq_or = lazy (constant "or") - let coq_not = lazy (constant "not") - let coq_iff = lazy (constant "iff") - let coq_True = lazy (constant "True") - let coq_False = lazy (constant "False") + let coq_and = lazy (init_constant "and") + let coq_or = lazy (init_constant "or") + let coq_not = lazy (init_constant "not") + let coq_iff = lazy (init_constant "iff") + let coq_True = lazy (init_constant "True") + let coq_False = lazy (init_constant "False") let coq_cons = lazy (constant "cons") let coq_nil = lazy (constant "nil") let coq_list = lazy (constant "list") - let coq_O = lazy (constant "O") - let coq_S = lazy (constant "S") - let coq_nat = lazy (constant "nat") + let coq_O = lazy (init_constant "O") + let coq_S = lazy (init_constant "S") + let coq_nat = lazy (init_constant "nat") let coq_NO = lazy (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]] "N0") @@ -205,7 +206,7 @@ struct let coq_Zge = lazy (constant "Zge") let coq_Zle = lazy (constant "Zle") let coq_Zlt = lazy (constant "Zlt") - let coq_Eq = lazy (constant "eq") + let coq_Eq = lazy (init_constant "eq") let coq_Zplus = lazy (constant "Zplus") let coq_Zminus = lazy (constant "Zminus") diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index e037ee8bf..02d70da74 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -162,12 +162,11 @@ 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_arith_modules @ [logic_dir] @ zarith_base_modules + init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let init_arith_constant = gen_constant_in_modules "Omega" init_arith_modules +let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules (* Zarith *) @@ -268,17 +267,17 @@ let coq_Zge = lazy (constant "Zge") let coq_Zlt = lazy (constant "Zlt") (* Peano/Datatypes *) -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") +let coq_le = lazy (init_constant "le") +let coq_lt = lazy (init_constant "lt") +let coq_ge = lazy (init_constant "ge") +let coq_gt = lazy (init_constant "gt") +let coq_minus = lazy (init_constant "minus") +let coq_plus = lazy (init_constant "plus") +let coq_mult = lazy (init_constant "mult") +let coq_pred = lazy (init_constant "pred") +let coq_nat = lazy (init_constant "nat") +let coq_S = lazy (init_constant "S") +let coq_O = lazy (init_constant "O") (* Compare_dec/Peano_dec/Minus *) let coq_pred_of_minus = lazy (constant "pred_of_minus") diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 2978d699e..796b3c7d1 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -56,17 +56,19 @@ let coq_modules = @ [module_refl_path] @ [module_refl_path@["ZOmega"]] + +let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules (* Logic *) -let coq_eq = lazy(constant "eq") -let coq_refl_equal = lazy(constant "refl_equal") -let coq_and = lazy(constant "and") -let coq_not = lazy(constant "not") -let coq_or = lazy(constant "or") -let coq_True = lazy(constant "True") -let coq_False = lazy(constant "False") -let coq_I = lazy(constant "I") +let coq_eq = lazy(init_constant "eq") +let coq_refl_equal = lazy(init_constant "eq_refl") +let coq_and = lazy(init_constant "and") +let coq_not = lazy(init_constant "not") +let coq_or = lazy(init_constant "or") +let coq_True = lazy(init_constant "True") +let coq_False = lazy(init_constant "False") +let coq_I = lazy(init_constant "I") (* ReflOmegaCore/ZOmega *) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 205bef6d5..9617d4091 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -439,11 +439,11 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | _, _ => false end. -Add Morphism (pow_pos rmul) : pow_morph. +Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph. intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. Qed. -Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph. +Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph. intros x y H [|p];simpl;auto. apply pow_morph;trivial. Qed. (* |