From 1e485645ef6481a856e8a67477f186519fb8ec9d Mon Sep 17 00:00:00 2001
From: coq
Date: Sat, 5 Oct 2002 11:03:20 +0000
Subject: Lazy experimentale temporaire...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml4 | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'contrib/xml/xmlcommand.ml4')

diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 14d0f94ac0..8710a9e1fa 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -739,7 +739,9 @@ let print (_,qid as locqid) fn =
         begin
          match val0 with
             None ->   print_axiom id typ [] hyps env inner_types
-          | Some c -> print_definition id c typ [] hyps env inner_types
+          | Some lc -> 
+	      let c = Lazy.force_val lc in
+	      print_definition id c typ [] hyps env inner_types
         end
     | Ln.IndRef (kn,_) ->
        let sp = Nt.sp_of_global None (Ln.IndRef(kn,0)) in  
@@ -856,7 +858,9 @@ let print_object lobj id (sp,kn) dn fv env =
             begin
              match val0 with
                 None -> print_axiom id typ fv hyps env inner_types
-              | Some c -> print_definition id c typ fv hyps env inner_types
+              | Some lc -> 
+		  let c = Lazy.force_val lc in
+		  print_definition id c typ fv hyps env inner_types
             end
       | "INDUCTIVE" ->
            let
-- 
cgit v1.2.3