From 640bf0dda4a4880aeb525d1460dc91f5041aa626 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 29 Apr 2016 02:25:12 +0200 Subject: Possibility to embed any Coq proof in certificates (not tested yet) --- src/trace/smtCertif.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/trace/smtCertif.ml') 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 _ -> [] -- cgit