diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-29 16:11:00 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-29 16:11:00 +0200 |
commit | cd1adfe2d51d05381a1044fb5a0086c608184ca9 (patch) | |
tree | 7a0828ac04b56ce7d764a10b339813cc95a6034d /engine/evd.ml | |
parent | ebc07e5741fab0df15a8de56fc69397a7d164ce9 (diff) | |
parent | b5d88066acbcebf598474e0d854b16078f4019ce (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'engine/evd.ml')
-rw-r--r-- | engine/evd.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 69ca45444..bde0182cc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -643,6 +643,7 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = + (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -1410,7 +1411,16 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = - let env = Namegen.make_all_name_different env in + let env = + (** We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + 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 + in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr_env env t1 ++ spc () ++ str (match pbty with |