Imported Upstream version 8.5~beta1+dfsg

1 files changed, 43 insertions, 35 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index df4c0ebc..749e0d2b 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -17,19 +17,21 @@ open Term
 open Indrec
 open Declarations
 open Typeops
-open Termops
 open Ind_tables
 
 (* Induction/recursion schemes *)
 
 let optimize_non_type_induction_scheme kind dep sort ind =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   if check_scheme kind ind then
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        apropriate type *)
-    let cte = find_scheme kind ind in
-    let c = mkConst cte in
-    let t = type_of_constant (Global.env()) cte in
+    let cte, eff = find_scheme kind ind in
+    let sigma, cte = Evd.fresh_constant_instance env sigma cte in
+    let c = mkConstU cte in
+    let t = type_of_constant_in (Global.env()) cte in
     let (mib,mip) = Global.lookup_inductive ind in
     let npars =
       (* if a constructor of [ind] contains a recursive call, the scheme
@@ -39,28 +41,42 @@ let optimize_non_type_induction_scheme kind dep sort ind =
 	mib.mind_nparams_rec
       else
 	mib.mind_nparams in
-    snd (weaken_sort_scheme (new_sort_in_family sort) npars c t)
+    let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
+    let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
+    let sigma, nf = Evarutil.nf_evars_and_universes sigma in
+      (nf c', Evd.evar_universe_context sigma), eff
   else
-    build_induction_scheme (Global.env()) Evd.empty ind dep sort
+    let mib,mip = Inductive.lookup_mind_specif env ind in
+    let ctx = Declareops.inductive_context mib in
+    let u = Univ.UContext.instance ctx in
+    let ctxset = Univ.ContextSet.of_context ctx in
+    let ectx = Evd.evar_universe_context_of ctxset in
+    let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+      (c, Evd.evar_universe_context sigma), Declareops.no_seff
 
 let build_induction_scheme_in_type dep sort ind =
-  build_induction_scheme (Global.env()) Evd.empty ind dep sort
-
+  let env = Global.env () in
+  let ctx = 
+    let mib,mip = Inductive.lookup_mind_specif env ind in
+      Declareops.inductive_context mib
+  in
+  let u = Univ.UContext.instance ctx in
+  let ctxset = Univ.ContextSet.of_context ctx in
+  let ectx = Evd.evar_universe_context_of ctxset in
+  let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+    c, Evd.evar_universe_context sigma
+ 
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (build_induction_scheme_in_type false InType)
+    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (build_induction_scheme_in_type false InType)
+    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (build_induction_scheme_in_type true InType)
-
-let rect_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_rect_dep"
-    (build_induction_scheme_in_type true InType)
+    (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -74,14 +90,6 @@ let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
 
-let ind_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_ind_dep"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp)
-
-let rec_scheme_kind_from_type =
-  declare_individual_scheme_object "_rec_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
 let rec_scheme_kind_from_prop =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
@@ -90,35 +98,35 @@ let rec_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
 
-let rec_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_rec_dep"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet)
-
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
-  build_case_analysis_scheme (Global.env()) Evd.empty ind dep sort
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, indu = Evd.fresh_inductive_instance env sigma ind in
+  let sigma, c = build_case_analysis_scheme env sigma indu dep sort in 
+    c, Evd.evar_universe_context sigma
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (build_case_analysis_scheme_in_type false InType)
+  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (build_case_analysis_scheme_in_type false InType)
+  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (build_case_analysis_scheme_in_type true InType)
+  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (build_case_analysis_scheme_in_type true InProp)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (build_case_analysis_scheme_in_type true InType)
+  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (build_case_analysis_scheme_in_type true InProp)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)