From 29794b8acf407518716f8c02c2ed20729f8802e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 13 Dec 2013 16:39:44 +0000
Subject: - Fix abstract forgetting about new constraints.

---
 plugins/funind/functional_principles_types.ml | 2 +-
 plugins/funind/recdef.ml                      | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 05cdd288c1..8a9c7d2e7b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -645,7 +645,7 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Universes.unsafe_constr_of_global (Nametab.global f)
+		 try fst (Universes.unsafe_constr_of_global (Nametab.global f))
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun,u = destConst  funs in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 50e7507f4d..8496bbbb35 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -75,7 +75,8 @@ let type_of_const t =
     Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
-let constr_of_global = Universes.unsafe_constr_of_global
+let constr_of_global x = 
+  fst (Universes.unsafe_constr_of_global x)
 
 let constant sl s = constr_of_global (find_reference sl s)
 
-- 
cgit v1.2.3