diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-29 02:25:12 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-29 02:25:12 +0200 |
| commit | 640bf0dda4a4880aeb525d1460dc91f5041aa626 (patch) | |
| tree | 68dfa3afc15c76979364cab6fe10c06f16d9d842 /src/trace/smtCertif.ml | |
| parent | d734e4eae47b0b7f13626053663d236faa7f69e6 (diff) | |
| download | smtcoq-640bf0dda4a4880aeb525d1460dc91f5041aa626.tar.gz smtcoq-640bf0dda4a4880aeb525d1460dc91f5041aa626.zip | |
Possibility to embed any Coq proof in certificates (not tested yet)
Diffstat (limited to 'src/trace/smtCertif.ml')
| -rw-r--r-- | src/trace/smtCertif.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 6a56c43..8ed87e4 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -108,6 +108,9 @@ type 'hform rule = (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform + (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *) + | Hole of 'hform + and 'hform clause = { id : clause_id; mutable kind : 'hform clause_kind; @@ -137,4 +140,5 @@ let used_clauses r = | ImmFlatten (c,_) | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c] | True | False | BuildDef _ | BuildDef2 _ | BuildProj _ | EqTr _ | EqCgr _ | EqCgrP _ - | LiaMicromega _ | LiaDiseq _ -> [] + | LiaMicromega _ | LiaDiseq _ + | Hole _ -> [] |