Rename files in funind to respect new conventions

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

7 files changed, 5 insertions, 5 deletions

diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0616007950..ce224d1aac 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -6,7 +6,7 @@ open Glob_term
 open Libnames
 open Indfun_common
 open Util
-open Rawtermops
+open Glob_termops
 
 let observe strm =
   if do_observe ()
diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 5c91292bad..5c91292bad 100644
--- a/plugins/funind/rawterm_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/glob_termops.ml
index 0cf91f38c0..0cf91f38c0 100644
--- a/plugins/funind/rawtermops.ml
+++ b/plugins/funind/glob_termops.ml
diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/glob_termops.mli
index b6c407a240..b6c407a240 100644
--- a/plugins/funind/rawtermops.mli
+++ b/plugins/funind/glob_termops.mli
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6e063d3c17..f23fcd6134 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -300,7 +300,7 @@ let generate_principle  on_error
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
   try
     (* We then register the Inductive graphs of the functions  *)
-    Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
+    Glob_term_to_relation.build_inductive names funs_args funs_types recdefs;
     if do_built
     then
       begin
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f757bafcbc..7c32c1d20c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -21,7 +21,7 @@ open Termops
 open Declarations
 open Environ
 open Glob_term
-open Rawtermops
+open Glob_termops
 
 (** {1 Utilities}  *)
 
diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib
index 31818c3992..ec1f5436ca 100644
--- a/plugins/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mllib
@@ -1,7 +1,7 @@
 Indfun_common
-Rawtermops
+Glob_termops
 Recdef
-Rawterm_to_relation
+Glob_term_to_relation
 Functional_principles_proofs
 Functional_principles_types
 Invfun