diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-18 18:01:20 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-18 18:01:20 +0100 |
| commit | bfce2747a747f48465fe32c3d29304ca6e774f25 (patch) | |
| tree | 6baf459718c380e90b76b5938e625ca0272a58e4 /src/lia | |
| parent | 23539f231727113d53e4fdeae531d048b21730ae (diff) | |
| download | smtcoq-bfce2747a747f48465fe32c3d29304ca6e774f25.tar.gz smtcoq-bfce2747a747f48465fe32c3d29304ca6e774f25.zip | |
Light port to Coq 8.5 under progress
Diffstat (limited to 'src/lia')
| -rw-r--r-- | src/lia/Lia.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v index 282523a..13a2405 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -473,7 +473,7 @@ Section certif. Fixpoint bounded_pexpr (p:positive) (pe:PExpr Z) := match pe with | PEc _ => true - | PEX x => Zlt_bool (Zpos x) (Zpos p) + | @PEX _ x => Zlt_bool (Zpos x) (Zpos p) | PEadd pe1 pe2 | PEsub pe1 pe2 | PEmul pe1 pe2 => bounded_pexpr p pe1 && bounded_pexpr p pe2 @@ -486,7 +486,7 @@ Section certif. Fixpoint bounded_bformula (p:positive) (bf:BFormula (Formula Z)) := match bf with - | TT | FF | X _ => true + | @TT _ | @FF _ | @X _ _ => true | A f => bounded_formula p f | Cj bf1 bf2 | D bf1 bf2 |