diff options
| author | Gaëtan Gilbert | 2019-06-17 22:57:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-17 22:57:33 +0200 |
| commit | 459fc67f4a40ff82a7694f9afafb3ac303d74554 (patch) | |
| tree | 9c1607700b3689c36de0daf0427f5e95aeb5b55c /vernac | |
| parent | d886dff0857702fc4524779980ee6b7e9688c1d4 (diff) | |
| parent | 621201858125632496fd11f431529187d69cfdc6 (diff) | |
Merge PR #10362: Kernel-side delaying of polymorphic opaque constants
Reviewed-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 4 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 4455a2d27a..d7cb9dc727 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) | _ -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 059d8a7c56..5b829917cb 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -93,7 +93,7 @@ let retrieve_first_recthm uctx = function (* we get the right order somehow but surely it could be enforced in a better way *) let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in - let map (c, ctx) = Vars.subst_instance_constr inst c in + let map (c, _, _) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false |