diff options
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | pretyping/heads.ml (renamed from library/heads.ml) | 2 | ||||
| -rw-r--r-- | pretyping/heads.mli (renamed from library/heads.mli) | 0 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 |
4 files changed, 2 insertions, 2 deletions
diff --git a/library/library.mllib b/library/library.mllib index 2ac4266fc0..9cacaba4a7 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -14,6 +14,5 @@ Kindops Dischargedhypsmap Goptions Decls -Heads Keys Coqlib diff --git a/library/heads.ml b/pretyping/heads.ml index d9d650ac07..18fc08d61a 100644 --- a/library/heads.ml +++ b/pretyping/heads.ml @@ -128,7 +128,7 @@ let compute_head = function let env = Global.env() in let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in - let body = + let body = if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in diff --git a/library/heads.mli b/pretyping/heads.mli index 421242996c..421242996c 100644 --- a/library/heads.mli +++ b/pretyping/heads.mli diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 3d9b5d3cfc..5da5aff449 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -14,6 +14,7 @@ Find_subterm Evardefine Evarsolve Recordops +Heads Evarconv Typing Miscops |