aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/interface/xlate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f09a8595b..0a9dffb9d 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