From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 13 Jun 2018 00:22:57 +0200 Subject: Remove reference name type. reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. --- interp/constrexpr_ops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 1c2348457..46aef1c78 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -41,7 +41,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option (** {6 Constructors}*) val mkIdentC : Id.t -> constr_expr -val mkRefC : reference -> constr_expr +val mkRefC : qualid -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr @@ -61,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list - (** {6 Destructors}*) -val coerce_reference_to_id : reference -> Id.t +val coerce_reference_to_id : qualid -> Id.t (** FIXME: nothing to do here *) val coerce_to_id : constr_expr -> lident -- cgit v1.2.3