80516bb format+gadts: make format types "relational" to fix %(...%) typing

Authored and Committed by Gabriel Scherer 9 years ago
    format+gadts: make format types "relational" to fix %(...%) typing
    
    See the long comment in pervasives.ml for an explanation of the
    change. The short summary is that we need to prove more elaborate
    properties between the format types involved in the typing of %(...%),
    and that proving things by writing GADT functions in OCaml reveals
    that Coq's Ltac is a miracle of usability.
    
    Proofs on OCaml GADTs are runtime functions that do have a runtime
    semantics: it is legitimate to hope that those proof computations are
    as simple as possible, but the current implementation was optimized
    for feasability, not simplicity. François Bobot has some interesting
    suggestions to simplify the reasoning part (with more equality
    reasoning where I used transitivity and symmetry of the
    relation profusely), which may make the code simpler in the future
    (and possibly more efficient: the hope is that only %(...%) users will
    pay a proof-related cost).
    
    git-svn-id: http://caml.inria.fr/svn/ocaml/version/4.02@14898 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
    
        
file modified
+0 -0
file modified
+0 -0
file modified
+0 -0
file modified
+124 -53
file modified
+275 -62
file modified
+20 -3
file modified
+252 -52
file modified
+190 -136
file modified
+21 -78
file modified
+6 -14