From 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Nov 2013 11:31:22 +0100
Subject: - Fix bug preventing apply from unfolding Fixpoints. - Remove
 Universe Polymorphism flags everywhere. - Properly infer, discharge template
 arities and fix substitution inside them (kernel code to check for
 correctness). - Fix tactics that were supposing universe polymorphic
 constants/inductives to be parametric on that status. Required to make
 interp_constr* return the whole evar universe context now. - Fix the
 univ/level/instance hashconsing to respect the fact that marshalling doesn't
 preserve sharing, sadly losing most of its benefits. Short-term solution is
 to add hashes to these for faster comparison, longer term requires rewriting
 all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v
---
 plugins/funind/functional_principles_types.ml | 4 ++--
 plugins/funind/invfun.ml                      | 2 +-
 plugins/funind/recdef.ml                      | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8a9c7d2e7b..a8876c75b1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -554,7 +554,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
     let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
-    let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*)
+    let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
       List.map (* we can now compute the other principles *)
@@ -597,7 +597,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	   in
 	   {const with
 	      Entries.const_entry_body = 
-                (Future.from_val (princ_body,Declareops.no_seff));
+                (Future.from_val (Term_typing.mk_pure_proof princ_body));
 	      Entries.const_entry_type = Some scheme_type
 	   }
       )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b68d9762ef..072b1ce005 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type )
+		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
 	    )
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8496bbbb35..4390143619 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1376,7 +1376,7 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    open_new_goal start_proof (Evd.get_universe_context_set sigma)
+    open_new_goal start_proof (Evd.universe_context_set sigma)
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
-- 
cgit v1.2.3