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/firstorder/sequent.ml | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

(limited to 'plugins/firstorder/sequent.ml')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 28599179..2a527da9 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -8,13 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open EConstr
-open CErrors
 open Util
+open Pp
+open CErrors
+open Names
+open EConstr
 open Formula
 open Unify
-open Globnames
-open Pp
 
 let newcnt ()=
   let cnt=ref (-1) in
@@ -56,7 +56,7 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-type h_item = global_reference * (int*Constr.t) option
+type h_item = GlobRef.t * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -77,17 +77,17 @@ module CM=Map.Make(Constr)
 module History=Set.Make(Hitem)
 
 let cm_add sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
 
 let cm_remove sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in
-    let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
+    let l0=List.filter (fun id-> not (GlobRef.equal id nam)) l in
       match l0 with
 	  []->CM.remove typ cm
 	| _ ->CM.add typ l0 cm
@@ -97,7 +97,7 @@ module HP=Heap.Functional(OrderedFormula)
 
 type t=
     {redexes:HP.t;
-     context:(global_reference list) CM.t;
+     context:(GlobRef.t list) CM.t;
      latoms:constr list;
      gl:types;
      glatom:constr option;
@@ -117,7 +117,7 @@ let lookup sigma item seq=
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
 	  History.exists p seq.history
 
 let add_formula env sigma side nam t seq =
@@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq=
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
-let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)
 
 (*let rev_left seq=
   try
@@ -187,9 +187,9 @@ let empty_seq depth=
 
 let expand_constructor_hints =
   List.map_append (function
-    | IndRef ind ->
+    | GlobRef.IndRef ind ->
         List.init (Inductiveops.nconstructors ind)
-          (fun i -> ConstructRef (ind,i+1))
+          (fun i -> GlobRef.ConstructRef (ind,i+1))
     | gr ->
 	[gr])
 
@@ -197,7 +197,7 @@ let extend_with_ref_list env sigma l seq =
   let l = expand_constructor_hints l in
   let f gr (seq, sigma) =
     let sigma, c = Evd.fresh_global env sigma gr in
-    let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in
+    let sigma, typ= Typing.type_of env sigma c in
       (add_formula env sigma Hyp gr typ seq, sigma) in
     List.fold_right f l (seq, sigma)
 
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
-- 
cgit v1.2.3