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

---
 proofs/evar_refiner.ml | 42 +++++++++++++++++++++++++-----------------
 1 file changed, 25 insertions(+), 17 deletions(-)

(limited to 'proofs/evar_refiner.ml')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 29cad063..0d197c92 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.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 CErrors
@@ -13,35 +15,41 @@ open Evd
 open Evarutil
 open Evarsolve
 open Pp
+open Glob_term
+open Ltac_pretype
 
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
 
-let depends_on_evar evk _ (pbty,_,t1,t2) =
-  try Evar.equal (head_evar t1) evk
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
+let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
+  try Evar.equal (head_evar sigma t1) evk
   with NoHeadEvar ->
-  try Evar.equal (head_evar t2) evk
+  try Evar.equal (head_evar sigma t2) evk
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c env evd =
-  if Termops.occur_evar evk c then
+  if Termops.occur_evar evd evk c then
     Pretype_errors.error_occur_check env evd evk c;
-  let evd = define evk c evd in
-  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+  let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
+	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
     | Success evd -> evd
-    | UnifFailure _ -> error "Instance does not satisfy the constraints."
+    | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
 
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
-    error "Instantiate called on already-defined evar";
+    user_err Pp.(str "Instantiate called on already-defined evar");
   let env = Evd.evar_filtered_env evi in
   let sigma',typed_c =
     let flags = {
@@ -51,11 +59,11 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
+      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err_loc
-        (loc,"", str "Instance is not well-typed in the environment of " ++
-                 pr_existential_key sigma evk ++ str ".")
+      user_err ?loc 
+                (str "Instance is not well-typed in the environment of " ++
+                 Termops.pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
-- 
cgit v1.2.3