From 55fb4d43e1113608f77f8f2b375e9daffe4fe3dc Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 12 Feb 2004 16:39:43 +0000
Subject: lazy was translated to cbv, obviously wrong

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5322 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f09a8595bb..0a9dffb9df 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -753,7 +753,7 @@ and xlate_red_tactic =
      CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
   | Lazy flag_list ->
      let conv_flags, red_ids = get_flag flag_list in
-     CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
+     CT_lazy (CT_conversion_flag_list conv_flags, red_ids)
   | Unfold unf_list ->
      let ct_unf_list = List.map xlate_one_unfold_block unf_list in
      (match ct_unf_list with
-- 
cgit v1.2.3