Rename rawterm.ml into glob_term.ml

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

9 files changed, 17 insertions, 17 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index bb4d7423f..77eeac64b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -512,13 +512,13 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
-                                        Rawterm.NoBindings))]
+                                        Glob_term.NoBindings))]
                                 None
                                 (None,None)
 		                None;
                      intro_using freshm;
                      new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
-                                    Rawterm.NoBindings))]
+                                    Glob_term.NoBindings))]
                                 None
                                 (None,None)
 		                None;
@@ -539,7 +539,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                            in
                             avoid := fresht::(!avoid);
                             (new_destruct false [Tacexpr.ElimOnConstr
-                                      ((mkVar freshz,Rawterm.NoBindings))]
+                                      ((mkVar freshz,Glob_term.NoBindings))]
                                   None
                                   (None, Some (dl,Genarg.IntroOrAndPattern [[
                                     dl,Genarg.IntroIdentifier fresht;
@@ -650,13 +650,13 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      new_induct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshn),Rawterm.NoBindings)]
+                                    ((mkVar freshn),Glob_term.NoBindings)]
                                 None
                                 (None,None)
 		                None;
                      intro_using freshm;
                      new_destruct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshm),Rawterm.NoBindings)]
+                                    ((mkVar freshm),Glob_term.NoBindings)]
                                 None
                                 (None,None)
 		                None;
@@ -665,7 +665,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
                      tclTRY (
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
+                     Equality.inj [] false (mkVar freshz,Glob_term.NoBindings);
 		     intros; simpl_in_concl;
                      Auto.default_auto;
                      tclREPEAT (
@@ -810,7 +810,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
 	)
 	  (tclTHEN
 	    (new_destruct false [Tacexpr.ElimOnConstr
-              (eqbnm,Rawterm.NoBindings)]
+              (eqbnm,Glob_term.NoBindings)]
               None
               (None,None)
 	      None)
@@ -820,7 +820,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
           avoid := freshH2::(!avoid);
 	  tclTHENS (
 	    new_destruct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshH),Rawterm.NoBindings)]
+                                    ((mkVar freshH),Glob_term.NoBindings)]
                                 None
                                 (None,Some (dl,Genarg.IntroOrAndPattern [
                                     [dl,Genarg.IntroAnonymous];
@@ -851,7 +851,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
 	                      all_occurrences false
                               (List.hd !avoid)
                               ((mkVar (List.hd (List.tl !avoid))),
-                                Rawterm.NoBindings
+                                Glob_term.NoBindings
                               )
                               true;
               Equality.discr_tac false None
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index bf029f419..f5a450a5c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -21,7 +21,7 @@ open Typeclasses_errors
 open Typeclasses
 open Libnames
 open Constrintern
-open Rawterm
+open Glob_term
 open Topconstr
 (*i*)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2e6fd8f49..b37a27faf 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -319,7 +319,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun ((_,indname),_,ar,lc) -> {
     ind_name = indname;
-    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
+    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.RType None)) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 04e0b352c..1c677de95 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -26,7 +26,7 @@ open Reduction
 open Cases
 open Logic
 open Printer
-open Rawterm
+open Glob_term
 open Evd
 
 let pr_lconstr c = quote (pr_lconstr c)
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index a1464b80c..b26c3b88d 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -11,7 +11,7 @@ open Names
 open Term
 open Environ
 open Libnames
-open Rawterm
+open Glob_term
 open Genarg
 open Vernacexpr
 open Ind_tables
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7564ee8ea..e3aaaa5e9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -19,7 +19,7 @@ open Summary
 open Constrintern
 open Vernacexpr
 open Pcoq
-open Rawterm
+open Glob_term
 open Libnames
 open Tok
 open Lexer
diff --git a/toplevel/search.ml b/toplevel/search.ml
index b2e33d1d3..d07743380 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Nameops
 open Term
-open Rawterm
+open Glob_term
 open Declarations
 open Libobject
 open Declare
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 797fc79c6..1b8271c89 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -134,7 +134,7 @@ type option_ref_value =
   | StringRefValue of string
   | QualidRefValue of reference
 
-type sort_expr = Rawterm.rawsort
+type sort_expr = Glob_term.rawsort
 
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index dd947fcda..a6ef73617 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -15,7 +15,7 @@ open System
 open Names
 open Term
 open Environ
-open Rawterm
+open Glob_term
 open Libnames
 open Nametab
 open Detyping