diff options
| -rw-r--r-- | test-suite/output/unification.out | 11 | ||||
| -rw-r--r-- | test-suite/output/unification.v | 12 | ||||
| -rw-r--r-- | vernac/himsg.ml | 1 |
3 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out new file mode 100644 index 0000000000..dfd755da61 --- /dev/null +++ b/test-suite/output/unification.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +In environment +x : T +T : Type +a : T +Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate +"?X" because "T" is not in its scope: available arguments are +"x" "C a"). +The command has indeed failed with message: +The term "id" has type "ID" while it is expected to have type +"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v new file mode 100644 index 0000000000..ff99f2e23c --- /dev/null +++ b/test-suite/output/unification.v @@ -0,0 +1,12 @@ +(* Unification error tests *) + +Module A. + +(* Check regression of an UNBOUND_REL bug *) +Inductive T := C : forall {A}, A -> T. +Fail Check fun x => match x return ?[X] with C a => a end. + +(* Bug #3634 *) +Fail Check (id:Type -> _). + +End A. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 19ec0a3642..085689be0a 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -297,6 +297,7 @@ let explain_unification_error env sigma p1 p2 = function strbrk " with term " ++ pr_leconstr_env env sigma rhs ++ strbrk " that would depend on itself"] | NotClean ((evk,args),env,c) -> + let env = make_all_name_different env sigma in [str "cannot instantiate " ++ quote (pr_existential_key sigma evk) ++ strbrk " because " ++ pr_leconstr_env env sigma c ++ strbrk " is not in its scope" ++ |