global_reference migrated from Libnames to new Globnames, less deps in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 17 insertions, 10 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a3bb2eee96..046b65ee8f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -15,6 +15,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
+open Globnames
 open Misctypes
 
 let msgnl = Pp.msgnl
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b38503cb94..21f77e438d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -101,7 +101,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn =
     fst (match princ_type_info.indref with
-	   | Some (Libnames.IndRef ind) -> ind
+	   | Some (Globnames.IndRef ind) -> ind
 	   | _ -> error "Not a valid predicate"
 	)
   in
@@ -660,7 +660,7 @@ let build_scheme fas =
 	    let f_as_constant =
 	      try
 		match Nametab.global f with
-		  | Libnames.ConstRef c -> c
+		  | Globnames.ConstRef c -> c
 		  | _ -> Errors.error "Functional Scheme can only be used with functions"
 	      with Not_found ->
 	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
@@ -692,7 +692,7 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Libnames.constr_of_global (Nametab.global f)
+		 try Globnames.constr_of_global (Nametab.global f)
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun = destConst  funs in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index cf9b54a94f..d1fc8ef33d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -5,6 +5,7 @@ open Term
 open Glob_term
 open Glob_ops
 open Libnames
+open Globnames
 open Indfun_common
 open Errors
 open Util
@@ -971,7 +972,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in
+		    let jmeq = Globnames.IndRef (destInd (jmeq ())) in
 		    let ty' = Pretyping.understand Evd.empty env ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
 		    let mib,_ = Global.lookup_inductive ind in
@@ -981,7 +982,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    let rt_typ =
 		       GApp(Pp.dummy_loc,
-			    GRef (Pp.dummy_loc,Libnames.IndRef ind),
+			    GRef (Pp.dummy_loc,Globnames.IndRef ind),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6433fe37cc..8967a3ec85 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -441,7 +441,7 @@ let rec pattern_to_term  = function
       let patl_as_term =
 	List.map pattern_to_term patternl
       in
-      mkGApp(mkGRef(Libnames.ConstructRef constr),
+      mkGApp(mkGRef(Globnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 761337b07e..437ba225d6 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -17,7 +17,7 @@ val pattern_to_term : cases_pattern -> glob_constr
    Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-val mkGRef : Libnames.global_reference -> glob_constr
+val mkGRef : Globnames.global_reference -> glob_constr
 val mkGVar : Names.identifier -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d3f56341ff..2a6a7dea32 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -5,6 +5,7 @@ open Term
 open Pp
 open Indfun_common
 open Libnames
+open Globnames
 open Glob_term
 open Declarations
 open Misctypes
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index c0b72f0b36..654d42ee16 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -23,4 +23,4 @@ val functional_induction :
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
-val make_graph :  Libnames.global_reference -> unit
+val make_graph :  Globnames.global_reference -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index de7e179571..026b9ad0ec 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,6 +1,7 @@
 open Names
 open Pp
 open Libnames
+open Globnames
 open Refiner
 open Hiddentac 
 let mk_prefix pre id = id_of_string (pre^(string_of_id id))
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index bb59a5c9cc..8f80c072c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -117,9 +117,9 @@ val h_intros: Names.identifier list -> Proof_type.tactic
 val h_id :  Names.identifier
 val hrec_id :  Names.identifier
 val acc_inv_id :  Term.constr Util.delayed
-val ltof_ref : Libnames.global_reference Util.delayed
+val ltof_ref : Globnames.global_reference Util.delayed
 val well_founded_ltof : Term.constr Util.delayed
 val acc_rel : Term.constr Util.delayed
 val well_founded : Term.constr Util.delayed
-val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference 
+val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
 val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4d072eca56..b0897c61e5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -13,6 +13,7 @@ open Names
 open Term
 open Pp
 open Libnames
+open Globnames
 open Tacticals
 open Tactics
 open Indfun_common
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ebe5cebd2e..af7506103d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -9,6 +9,7 @@
 (* Merging of induction principles. *)
 
 open Libnames
+open Globnames
 open Tactics
 open Indfun_common
 open Errors
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0b61c5f858..2005a90e31 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -16,6 +16,7 @@ open Entries
 open Pp
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Errors
 open Util