From 886a9c2fb25e32bd87b3fce38023b3e701134d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 27 Dec 2017 20:22:23 +0100 Subject: [econstr] Continue consolidation of EConstr API under `interp`. This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag. --- printing/ppconstr.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 3c7095505..dedad1990 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -701,13 +701,16 @@ let tag_var = tag Tag.variable | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us | c -> pr prec c - let transf env c = + let transf env sigma c = if !Flags.beautify_file then - let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in + let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr_expr prec c = pr prec (transf (Global.env()) c) + let pr_expr prec c = + let env = Global.env () in + let sigma = Evd.from_env env in + pr prec (transf env sigma c) let pr_simpleconstr = pr_expr lsimpleconstr -- cgit v1.2.3