From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 14 Nov 2017 22:36:47 +0100
Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel
 style.

In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.

This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.

A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
---
 plugins/firstorder/sequent.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

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

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7c612c0d8..0c752d4a4 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
@@ -87,7 +87,7 @@ let cm_remove sigma typ nam cm=
   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 =
@@ -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])
 
-- 
cgit v1.2.3