diff options
| author | Hugo Herbelin | 2017-07-13 12:21:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-23 12:57:48 +0100 |
| commit | 446b265f5d1f6e6828a7f653b1f648ebdf768321 (patch) | |
| tree | 97e5ac9077264c774e871b201137ae4871100a34 | |
| parent | 1b09c7b0802c85ea72931720a7cb4fbf9ab5e211 (diff) | |
Recognizing Z in romega up to conversion.
| -rw-r--r-- | plugins/romega/const_omega.ml | 12 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4717.v | 4 |
2 files changed, 7 insertions, 9 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5397b00656..7956be58ba 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -198,6 +198,7 @@ let parse_logic_rel c = match destructurate c with (* Binary numbers *) +let coq_Z = lazy (bin_constant "Z") let coq_xH = lazy (bin_constant "xH") let coq_xO = lazy (bin_constant "xO") let coq_xI = lazy (bin_constant "xI") @@ -238,7 +239,7 @@ end module Z : Int = struct -let typ = lazy (bin_constant "Z") +let typ = coq_Z let plus = lazy (z_constant "Z.add") let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") @@ -286,14 +287,9 @@ let parse_term t = (match recognize_Z t with Some t -> Tnum t | None -> Tother) | _ -> Tother -let pf_nf gl c = - EConstr.Unsafe.to_constr - (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) - let is_int_typ gl t = - match destructurate (pf_nf gl t) with - | Kapp("Z",[]) -> true - | _ -> false + Tacmach.New.pf_apply Reductionops.is_conv gl + (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) let parse_rel gl t = match destructurate t with diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 4562ed1f1a..1507fa4bf0 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,7 +19,7 @@ Proof. omega. Qed. -Require Import ZArith. +Require Import ZArith ROmega. Open Scope Z_scope. @@ -32,4 +32,6 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. + Undo. + romega. Qed. |