From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 21:51:23 +0200
Subject: Safer API for Global.body_of_constant and variants.

We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
---
 vernac/assumptions.ml | 4 ++--
 vernac/lemmas.ml      | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index db07bbd068..86bbf46a35 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -187,7 +187,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
-  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
   traverse_object accu body (ConstRef kn)
 | Ind ((mind, _) as ind, _) ->
   traverse_inductive accu mind (IndRef ind)
@@ -200,7 +200,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
     | Lambda(_,_,oty), Const (kn, _)
       when Vars.noccurn 1 oty &&
       not (Declareops.constant_has_body (lookup_constant kn)) ->
-        let body () = Global.body_of_constant_body (lookup_constant kn) in
+        let body () = Option.map fst (Global.body_of_constant_body (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 2eeaf4d5dc..cfd489ddef 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ let retrieve_first_recthm = function
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      (Global.body_of_constant_body cb, is_opaque cb)
+      let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
+      (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
-- 
cgit v1.2.3