Mentions légales du service

Skip to content
  • Sylvain Dailler's avatar
    Cherry picked from a commit of Julien Thierry that aims at improving the · 4756c1cd
    Sylvain Dailler authored
    Coq printer.
    Also adding the "pretty-printed" generated realization.
    
    
    
    N604-045 Coq code easier to read
    
    * src/printer/coq.ml
    Added indentation in Why3's Coq printer using the OCaml Format pretty
    printing module.
    Changed the display of logic formulas and terms only.
    
    (cherry picked from commit 3453a65e0e5fca7e3aa16e22915ee3f079daf1c6)
    
    Conflicts:
    	src/printer/coq.ml
    	src/transform/gnat_split_conj.ml
    4756c1cd