From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Jul 2003 14:01:58 +0000 (+0000)
Subject: Flattening application contexts uncorrectly changed the proof ids.
X-Git-Tag: LucaOK~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=735b9b35a70420d91d074e8add620f03d7100d1a

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 12b806162..2749708d2 100644
--- 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