Skip to content

GitLab

F
FloVer
Switch branch/tag
Find file Normal viewHistoryPermalink
Checker_extraction.v 282 Bytes
Newer Older
Heiko Becker's avatar
Renaming in Coq dev, move attic files to separate folder  
Heiko Becker committed
1 
Require Import Flover.CertificateChecker Flover.floverParser.
Heiko Becker's avatar
Simplify transScript by removing dead functions and add coq parser + extraction  
Heiko Becker committed
2 
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Heiko Becker's avatar
Enable unverified extraction of binary in Coq  
Heiko Becker committed
3
Heiko Becker's avatar
Fix Coq 8.7.2 compatobility  
Heiko Becker committed
4 
Extraction Language Ocaml.
Heiko Becker's avatar
Enable unverified extraction of binary in Coq  
Heiko Becker committed
5
Joachim Bard's avatar
support for additional conditions in precond  
Joachim Bard committed
6 
Extraction "./binary/CoqChecker.ml" runChecker.