diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-06 18:34:44 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-06 18:34:44 +0100 |
| commit | 00bf195620810ff5721a840f0a99417f092f5eee (patch) | |
| tree | 53eef376e9fff66b1f2ec2d13ce3bcd3a79b635c /src/extraction/zchaff_checker.ml | |
| parent | 48e123caddd6a4c4edd60d8f39b78a5421418f40 (diff) | |
| download | smtcoq-00bf195620810ff5721a840f0a99417f092f5eee.tar.gz smtcoq-00bf195620810ff5721a840f0a99417f092f5eee.zip | |
Update extraction (only ml)
Diffstat (limited to 'src/extraction/zchaff_checker.ml')
| -rw-r--r-- | src/extraction/zchaff_checker.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml index 60d0a38..eb28fe8 100644 --- a/src/extraction/zchaff_checker.ml +++ b/src/extraction/zchaff_checker.ml @@ -54,7 +54,7 @@ let to_coq to_lit (cstep, cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, cImmBuildProj,cImmBuildDef,cImmBuildDef2, cEqTr, cEqCgr, cEqCgrP, - cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl = + cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, cHole) confl = let step_to_coq c = match c.kind with | Res res -> |