diff options
| author | Gaëtan Gilbert | 2019-07-03 09:54:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 09:54:31 +0200 |
| commit | 73999ad6ba6c33783f27ffc705930cbc5c745728 (patch) | |
| tree | d2d12c00ef94e941bb3392ef119329f9d44d010b /pretyping | |
| parent | 0cc7e942cd04f7fd28336045e43345b47a48b7a5 (diff) | |
| parent | 62567575f4639aad44de93a88d9cc425a11d4a9e (diff) | |
Merge PR #10419: [api] Refactor most of `Decl_kinds`
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'pretyping')
| -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 = |