diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 13:23:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:55 +0200 |
| commit | b78a4f8afc6180c1d435258af681d354e211cab2 (patch) | |
| tree | dd77b9d47fe0cc7a0accc0360b9d0f5dc4ea9384 | |
| parent | 47389d31c0aa6fafa1c696b1e6f06059751a8217 (diff) | |
[pretyping] Remove seemingly unless check about "variable" opacity.
See discussion in #10417
| -rw-r--r-- | pretyping/heads.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/heads.ml b/pretyping/heads.ml index d65faecd19..870df62500 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -41,8 +41,7 @@ let rec compute_head env = function | Some c -> kind_of_head env c) | EvalVarRef id -> (match lookup_named id env with - | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head env c + | LocalDef (_,c,_) -> kind_of_head env c | _ -> RigidHead RigidOther) and kind_of_head env t = |