diff options
| author | Hugo Herbelin | 2015-07-16 09:32:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-16 09:40:08 +0200 |
| commit | 93579407f5795c117d6c6f1399396b690f80d723 (patch) | |
| tree | 701aad6c0994ae5e533d86847b67e8ea827abf30 | |
| parent | c57c7edbe517851c7309112f6eb5d8297f03e000 (diff) | |
Fixing anomaly #3743 while printing an error message involving evar constraints.
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
| -rw-r--r-- | library/nameops.ml | 5 | ||||
| -rw-r--r-- | library/nameops.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
3 files changed, 9 insertions, 3 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index 02b085a7ac..3a23ab97df 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -136,6 +136,11 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous +let name_max na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + let pr_lab l = str (Label.to_string l) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nameops.mli b/library/nameops.mli index 23432ae2fa..de1f99fe0f 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit val name_cons : Name.t -> Id.t list -> Id.t list val name_app : (Id.t -> Id.t) -> Name.t -> Name.t val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - +val name_max : Name.t -> Name.t -> Name.t val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 97b1b16455..64d1345c1f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -726,12 +726,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd,UnifUnivInconsistency p) | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) - | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty -> + | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)] + let na = Nameops.name_max n1 n2 in + evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then |