diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b19f8376c..ab0ce7e56 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,7 @@ let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in @@ -594,7 +594,7 @@ let gallina_print_context with_values = prec let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma trm in + let ntrm = red_fun env sigma (EConstr.of_constr trm) in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) |