diff options
| author | Gaëtan Gilbert | 2018-06-23 15:00:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 12:03:10 +0200 |
| commit | fb9003c7850c459d7a5981212d8ef87de877bd9f (patch) | |
| tree | 463bb0753a912ea2d0a7ab59518de820e20429a2 | |
| parent | 4ab54f3cca76632cb6e258c84abc259e15e9e9f8 (diff) | |
Move Heads to pretyping (is_projection will move to Recordops)
| -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 |