From b78a4f8afc6180c1d435258af681d354e211cab2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 13:23:08 +0200
Subject: [pretyping] Remove seemingly unless check about "variable" opacity.

See discussion in #10417
---
 pretyping/heads.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping')

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 =
-- 
cgit v1.2.3