diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /plugins/omega | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'plugins/omega')
-rw-r--r-- | plugins/omega/PreOmega.v | 8 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 23 | ||||
-rw-r--r-- | plugins/omega/g_omega.mlg (renamed from plugins/omega/g_omega.ml4) | 9 | ||||
-rw-r--r-- | plugins/omega/omega.ml | 2 |
4 files changed, 23 insertions, 19 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 59fd9b80..94a3d404 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:= Ltac zify_op_1 := match goal with + | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b @@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t := Ltac zify_nat_rel := match goal with (* I: equalities *) + | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) @@ -181,7 +183,7 @@ Ltac zify_nat_op := let t := eval compute in (Z.of_nat (S a)) in change (Z.of_nat (S a)) with t in H | _ => rewrite (Nat2Z.inj_succ a) in H - | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), hide [Z.of_nat (S a)] in this one hypothesis *) change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H end @@ -192,7 +194,7 @@ Ltac zify_nat_op := let t := eval compute in (Z.of_nat (S a)) in change (Z.of_nat (S a)) with t | _ => rewrite (Nat2Z.inj_succ a) - | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), hide [Z.of_nat (S a)] in the goal *) change (Z.of_nat (S a)) with (Z_of_nat' (S a)) end @@ -223,6 +225,7 @@ Ltac hide_Zpos t := Ltac zify_positive_rel := match goal with (* I: equalities *) + | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq positive ?a ?b) => apply Pos2Z.inj | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) @@ -348,6 +351,7 @@ Ltac hide_Z_of_N t := Ltac zify_N_rel := match goal with (* I: equalities *) + | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 51cd665f..e14c4e2e 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -18,8 +18,8 @@ open CErrors open Util open Names +open Constr open Nameops -open Term open EConstr open Tacticals.New open Tacmach.New @@ -29,7 +29,7 @@ open Libnames open Globnames open Nametab open Contradiction -open Misctypes +open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -38,15 +38,9 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) -let elim_id id = - Proofview.Goal.enter begin fun gl -> - simplest_elim (mkVar id) - end -let resolve_id id = Proofview.Goal.enter begin fun gl -> - apply (mkVar id) -end +let elim_id id = simplest_elim (mkVar id) -let timing timer_name f arg = f arg +let resolve_id id = apply (mkVar id) let display_time_flag = ref false let display_system_flag = ref false @@ -206,7 +200,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s) +let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules @@ -369,8 +363,11 @@ let coq_True = lazy (init_constant "True") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with - | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> +let evaluable_ref_of_constr s c = + let env = Global.env () in + let evd = Evd.from_env env in + match EConstr.kind evd (Lazy.force c) with + | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg index 170b937c..c3d063cf 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.mlg @@ -18,6 +18,8 @@ DECLARE PLUGIN "omega_plugin" +{ + open Ltac_plugin open Names open Coq_omega @@ -43,14 +45,15 @@ let omega_tactic l = (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) (omega_solver) +} TACTIC EXTEND omega -| [ "omega" ] -> [ omega_tactic [] ] +| [ "omega" ] -> { omega_tactic [] } END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.Id.to_string l) ] -| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] + { omega_tactic (List.map Names.Id.to_string l) } +| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] } END diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 2510c169..7bca7c70 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -178,7 +178,7 @@ let rec display_action print_var = function | DIVIDE_AND_APPROX (e1,e2,k,d) -> Printf.printf "Inequation E%d is divided by %s and the constant coefficient is \ - rounded by substracting %s.\n" e1.id (sbi k) (sbi d) + rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) | NOT_EXACT_DIVIDE (e,k) -> Printf.printf "Constant in equation E%d is not divisible by the pgcd \ |