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/trunk@14897 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

3 files changed, 0 insertions, 0 deletions

diff --git a/boot/ocamlc b/boot/ocamlc
index 77d85cc719..ba711c23ec 100755
--- a/boot/ocamlc
+++ b/boot/ocamlc
diff --git a/boot/ocamldep b/boot/ocamldep
index 0f81aae10b..8f2cdeed7a 100755
--- a/boot/ocamldep
+++ b/boot/ocamldep
diff --git a/boot/ocamllex b/boot/ocamllex
index d6c30bcdee..4afd4c898f 100755
--- a/boot/ocamllex
+++ b/boot/ocamllex