diff options
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 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) | _ -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7aba64fb93..cd8b17f681 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 |