Flattening application contexts uncorrectly changed the proof ids.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 12b806162b45abb816a90f3e7d9bca0f7225bc4f..2749708d2018ec609e8132f689d02f40ad9e781a 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -209,7 +209,6 @@ let flat seed p =
     else 
       let p1 =
         { p with
-          K.proof_id = gen_id seed;
           K.proof_context = []; 
           K.proof_apply_context = []
         } in