diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 001f3b5a6..d9d82faa2 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -323,7 +323,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | GLambda (_,x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = - if List.for_all (name_eq Anonymous) nl then None + if List.for_all (Name.equal Anonymous) nl then None else Some (dl,indsp,nl) in n, aliastyp, Some typ in |