The Coq mailing list

["austin.zhuang" <dyzz AT mail.ustc.edu.cn>]

Hi,
   I just read about extraction and was interested in how to use ocaml code
in Coq. I find "Declare ML Module" in reference manual, which is a way to
load ".cmo" file. But there is no more guides in the manual, so, can anyone
give a quick example of this?
  
    for example, I have "lib.ml":
      type data_type = |INT|FLOAT|DOUBLE
    
    How can I use this data_type definition in Coq? And Can I use functions
in ".cmo" file or even more?
    
    p.s. Would there be a part of how to write coq tactics in ocaml in the
future?
  
    Thanks!
                                                                              
                      
Austin Zhuang
                                                                              
                       
SSG@USTC
                                                                              
                    
-- 
View this message in context: 
http://www.nabble.com/Questions-about-%22Declare-ML-Module%22-etc-tp20538966p20538966.html
Sent from the Coq mailing list archive at Nabble.com.