diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evd.ml | 12 | ||||
-rw-r--r-- | engine/termops.ml | 4 | ||||
-rw-r--r-- | engine/termops.mli | 1 |
3 files changed, 16 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 diff --git a/engine/termops.ml b/engine/termops.ml index 5e65652c0..5327f1829 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -600,6 +600,10 @@ let collect_vars c = | _ -> fold_constr aux vars c in aux Id.Set.empty c +let vars_of_global_reference env gr = + let c, _ = Universes.unsafe_constr_of_global gr in + vars_of_global (Global.env ()) c + (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) diff --git a/engine/termops.mli b/engine/termops.mli index 7d6e99acc..c58e3728c 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -121,6 +121,7 @@ val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) +val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t val occur_term : constr -> constr -> bool (** Synonymous of dependent Substitution of metavariables *) |