diff options
| author | Pierre-Marie Pédrot | 2019-06-04 13:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:02 +0200 |
| commit | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (patch) | |
| tree | 8016562d06949b981a3e58e71103b02aea7f1c44 /vernac/assumptions.ml | |
| parent | 7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff) | |
Allow to delay polymorphic opaque constants.
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
Diffstat (limited to 'vernac/assumptions.ml')
| -rw-r--r-- | vernac/assumptions.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 9353ef3902..5c6a282894 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> |