From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/funind/indfun_common.ml | 38 ++++++++++++++++++--------------------
 1 file changed, 18 insertions(+), 20 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a0b9217c..4eee2c7a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -31,9 +31,7 @@ let id_of_name = function
     Name id -> id
   | _ -> raise Not_found
 
-let locate  ref =
-    let {CAst.v=qid} = qualid_of_reference ref in
-    Nametab.locate qid
+let locate qid = Nametab.locate qid
 
 let locate_ind ref =
   match locate ref with
@@ -109,7 +107,7 @@ let const_of_id id =
 
 let def_of_const t =
    match Constr.kind t with
-    Term.Const sp ->
+    Const sp ->
       (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
 	     | _ -> assert false)
@@ -117,7 +115,7 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
@@ -269,12 +267,12 @@ let subst_Function (subst,finfos) =
   in
   let function_constant' = do_subst_con finfos.function_constant in
   let graph_ind' = do_subst_ind finfos.graph_ind in
-  let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
-  let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
-  let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
-  let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
-  let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
-  let prop_lemma' =  Option.smartmap do_subst_con finfos.prop_lemma in
+  let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in
+  let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in
+  let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in
+  let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
+  let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
+  let prop_lemma' =  Option.Smart.map do_subst_con finfos.prop_lemma in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
@@ -302,12 +300,12 @@ let classify_Function infos = Libobject.Substitute infos
 let discharge_Function (_,finfos) =
   let function_constant' = Lib.discharge_con finfos.function_constant
   and graph_ind' = Lib.discharge_inductive finfos.graph_ind
-  and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
-  and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
-  and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
-  and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
-  and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
-  and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
+  and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
+  and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
+  and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
+  and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
+  and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
+  and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
   in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
@@ -471,7 +469,7 @@ let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -479,7 +477,7 @@ let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -492,7 +490,7 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
 let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
 
-let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
-- 
cgit v1.2.3