diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-30 00:41:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 (patch) | |
| tree | b89ce3f21a24c65a5ce199767d13182007b78a25 /engine/termops.ml | |
| parent | 1683b718f85134fdb0d49535e489344e1a7d56f5 (diff) | |
Namegen primitives now apply on evar constrs.
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ff1a0d9de..d8e712abc 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma = | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in - Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous + Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous in let names = EvMap.mapi base_id (undefined_map sigma) in let id = EvMap.find evk names in @@ -316,7 +316,7 @@ let print_env_short env = str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ str "[" ++ pr_sequence pr_rel_decl rc ++ str "]" -let pr_evar_constraints pbs = +let pr_evar_constraints sigma pbs = let pr_evconstr (pbty, env, t1, t2) = let env = (** We currently allow evar instances to refer to anonymous de @@ -326,10 +326,10 @@ let pr_evar_constraints pbs = stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming. *) - Namegen.make_all_name_different env + Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++ + print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ @@ -346,7 +346,7 @@ let pr_evar_map_gen with_univs pr_evars sigma = if List.is_empty conv_pbs then mt () else str "CONSTRAINTS:" ++ brk (0, 1) ++ - pr_evar_constraints conv_pbs ++ fnl () + pr_evar_constraints sigma conv_pbs ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else |