diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 15:14:44 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 15:14:44 +0100 |
| commit | a1a9f9d62dfe0e8dfb8c924a74e57c9f08b4f2d9 (patch) | |
| tree | 509449063db80688ad270b347ae0558cb8ab03bc /plugins/romega | |
| parent | f9b3414888aebd1186f53c46d737536670171ab6 (diff) | |
| parent | c5f9e3a03c1f089253622ec262adf931e6dc1ca2 (diff) | |
Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 32a1c07b2..337510ef1 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -197,6 +197,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") @@ -237,7 +238,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") @@ -285,14 +286,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 |