diff options
| author | Pierre-Marie Pédrot | 2016-11-11 19:52:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:44 +0100 |
| commit | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (patch) | |
| tree | adeb71808e2f4d6be1686071e79e96cf6761f3c0 /plugins/romega | |
| parent | 53fe23265daafd47e759e73e8f97361c7fdd331b (diff) | |
Tacmach API using EConstr.
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4935fe4bbc..f2d91bad37 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -353,7 +353,7 @@ let parse_term t = let parse_rel gl t = try match destructurate t with | Kapp("eq",[typ;t1;t2]) - when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2) + when destructurate (Tacmach.pf_nf gl (EConstr.of_constr typ)) = Kapp("Z",[]) -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) |