diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/heads.ml | 2 | ||||
| -rw-r--r-- | library/misctypes.ml | 6 |
2 files changed, 1 insertions, 7 deletions
diff --git a/library/heads.ml b/library/heads.ml index 198672a0a1..3d5f6a6ff0 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body + if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with diff --git a/library/misctypes.ml b/library/misctypes.ml index a3c887045e..cfae074843 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -112,9 +112,3 @@ type multi = | UpTo of int | RepeatStar | RepeatPlus - -type ('a, 'b) gen_universe_decl = { - univdecl_instance : 'a; (* Declared universes *) - univdecl_extensible_instance : bool; (* Can new universes be added *) - univdecl_constraints : 'b; (* Declared constraints *) - univdecl_extensible_constraints : bool (* Can new constraints be added *) } |