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

---
 pretyping/find_subterm.ml | 51 +++++++++++++++++++++++++++--------------------
 1 file changed, 29 insertions(+), 22 deletions(-)

(limited to 'pretyping/find_subterm.ml')

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4caa1e99..b1608703 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.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)         *)
 (************************************************************************)
 
 open Pp
@@ -11,11 +13,12 @@ open Util
 open CErrors
 open Names
 open Locus
-open Term
-open Nameops
+open EConstr
 open Termops
 open Pretype_errors
 
+module NamedDecl = Context.Named.Declaration
+
 (** Processing occurrences *)
 
 type occurrence_error =
@@ -28,14 +31,14 @@ let explain_invalid_occurrence l =
   ++ prlist_with_sep spc int l ++ str "."
 
 let explain_incorrect_in_value_occurrence id =
-  pr_id id ++ str " has no value."
+  Id.print id ++ str " has no value."
 
 let explain_occurrence_error = function
   | InvalidOccurrence l -> explain_invalid_occurrence l
   | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
 
 let error_occurrences_error e =
-  errorlabstrm "" (explain_occurrence_error e)
+  user_err  (explain_occurrence_error e)
 
 let error_invalid_occurrence occ =
   error_occurrences_error (InvalidOccurrence occ)
@@ -61,7 +64,10 @@ let proceed_with_occurrences f occs x =
 
 let map_named_declaration_with_hyploc f hyploc acc decl =
   let open Context.Named.Declaration in
-  let f = f (Some (get_id decl, hyploc)) in
+  let f acc typ =
+    let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
+    acc, typ
+  in
   match decl,hyploc with
   | LocalAssum (id,_), InHypValueOnly ->
       error_occurrences_error (IncorrectInValueOccurrence id)
@@ -80,10 +86,10 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
 
 exception SubtermUnificationError of subterm_unification_error
 
-exception NotUnifiable of (constr * constr * unification_error) option
+exception NotUnifiable of (EConstr.t * EConstr.t * unification_error) option
 
 type 'a testing_function = {
-  match_fun : 'a -> constr -> 'a;
+  match_fun : 'a -> EConstr.constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
@@ -94,7 +100,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -128,23 +134,23 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
-    map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+    map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
   (!pos, t')
 
-let replace_term_occ_modulo occs test bywhat t =
+let replace_term_occ_modulo evd occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
+    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
 
-let replace_term_occ_decl_modulo occs test bywhat d =
+let replace_term_occ_decl_modulo evd occs test bywhat d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo plocs like_first test bywhat)
+       (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -152,11 +158,12 @@ let replace_term_occ_decl_modulo occs test bywhat d =
 
 let make_eq_univs_test env evd c =
   { match_fun = (fun evd c' ->
-    let b, cst = Universes.eq_constr_universes_proj env c c' in
-      if b then
+    match EConstr.eq_constr_universes_proj env evd c c' with
+    | None -> raise (NotUnifiable None)
+    | Some cst ->
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise (NotUnifiable None)
-      else raise (NotUnifiable None));
+    );
   merge_fun = (fun evd _ -> evd);
   testing_state = evd;
   last_found = None
@@ -165,7 +172,7 @@ let make_eq_univs_test env evd c =
 let subst_closed_term_occ env evd occs c t =
   let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
-  let t' = replace_term_occ_modulo occs test bywhat t in
+  let t' = replace_term_occ_modulo evd occs test bywhat t in
     t', test.testing_state
 
 let subst_closed_term_occ_decl env evd occs c d =
@@ -175,6 +182,6 @@ let subst_closed_term_occ_decl env evd occs c d =
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
-- 
cgit v1.2.3