From 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 13:44:05 +0200
Subject: 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.
---
 vernac/assumptions.ml | 4 ++--
 vernac/lemmas.ml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

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
 
-- 
cgit v1.2.3