diff options
| author | Pierre-Marie Pédrot | 2016-11-21 12:13:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:34 +0100 |
| commit | 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd (patch) | |
| tree | 101bd3bc2e05eb52bfc142587d425f8920671b25 /printing | |
| parent | e09f3b44bb381854b647a6d9debdeddbfc49177e (diff) | |
Reductionops now return EConstrs.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index ab0ce7e56e..e66d3aafed 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,8 @@ 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 (EConstr.of_constr typ) + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in + let ccl = EConstr.Unsafe.to_constr ccl in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in @@ -595,6 +596,7 @@ let gallina_print_context with_values = let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = let ntrm = red_fun env sigma (EConstr.of_constr trm) in + let ntrm = EConstr.Unsafe.to_constr ntrm in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) |