From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 tactics/elimschemes.ml | 71 ++++++++++++++++++++++----------------------------
 1 file changed, 31 insertions(+), 40 deletions(-)

(limited to 'tactics/elimschemes.ml')

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 93073fdc..6bd4866c 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Created by Hugo Herbelin from contents related to inductive schemes
@@ -13,12 +15,12 @@
 
 (* This file builds schemes related to case analysis and recursion schemes *)
 
-open Term
+open Sorts
+open Constr
 open Indrec
 open Declarations
 open Typeops
 open Ind_tables
-open Sigma.Notations
 
 (* Induction/recursion schemes *)
 
@@ -47,26 +49,15 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let sigma, nf = Evarutil.nf_evars_and_universes sigma in
       (nf c', Evd.evar_universe_context sigma), eff
   else
-    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 = Evd.merge_universe_context sigma ectx in
-    let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
+    let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+    let sigma, c = build_induction_scheme env sigma pind dep sort in
       (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env 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 sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
-  let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
+  let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+  let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
@@ -81,38 +72,38 @@ let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
     (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
-let ind_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
-
-let ind_scheme_kind_from_prop =
-  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
-
-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 rec_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+  (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)
 
-let rec_scheme_kind_from_type =
-  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
 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 ind_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind_nodep"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)
+
+let ind_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
+  (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)
+
+let ind_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)
+
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
   let env = Global.env () in
-  let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in
-  let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in
-  let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep sort in
-    c, Evd.evar_universe_context (Sigma.to_evar_map sigma)
+  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"
-- 
cgit v1.2.3