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

29 files changed, 38 insertions, 38 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 440f92b7f..8a05736ca 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -25,7 +25,7 @@ open Matching
 open Tacmach
 open Proof_type
 open Pfedit
-open Rawterm
+open Glob_term
 open Evar_refiner
 open Tacred
 open Tactics
diff --git a/tactics/auto.mli b/tactics/auto.mli
index fa6f1d9ca..73249d43a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -30,7 +30,7 @@ type auto_tactic =
   | Unfold_nth of evaluable_global_reference          (** Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr   (** Hint Extern *)
 
-open Rawterm
+open Glob_term
 
 type pri_auto_tactic = {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index fb5b2f527..73f8fde29 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -17,7 +17,7 @@ open Tactics
 open Term
 open Termops
 open Util
-open Rawterm
+open Glob_term
 open Vernacinterp
 open Tacexpr
 open Mod_subst
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b42df0109..1cf41a70a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -25,7 +25,7 @@ open Tactics
 open Pattern
 open Clenv
 open Auto
-open Rawterm
+open Glob_term
 open Hiddentac
 open Typeclasses
 open Typeclasses_errors
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0433df28d..a3d43623e 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -15,7 +15,7 @@ open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
-open Rawterm
+open Glob_term
 
 (* Absurd *)
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index c02d691a0..b77b2721a 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Proof_type
-open Rawterm
+open Glob_term
 open Genarg
 
 val absurd                      : constr -> tactic
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index e1e04c8ef..f9c316955 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -116,7 +116,7 @@ open Term
 open Environ
 open Reduction
 open Proof_type
-open Rawterm
+open Glob_term
 open Tacmach
 open Refiner
 open Tactics
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 47c7214f1..1bdeed6aa 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -24,5 +24,5 @@ val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
   Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
-    Rawterm.patvar list * Pattern.constr_pattern -> int ->
+    Glob_term.patvar list * Pattern.constr_pattern -> int ->
       glob_tactic_expr -> unit
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 6f4d90ab4..ed8da10a0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -25,7 +25,7 @@ open Tactics
 open Pattern
 open Clenv
 open Auto
-open Rawterm
+open Glob_term
 open Hiddentac
 
 let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
diff --git a/tactics/elim.mli b/tactics/elim.mli
index fcf469e2c..48a7ca68c 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -30,5 +30,5 @@ val h_decompose       : inductive list -> constr -> tactic
 val h_decompose_or    : constr -> tactic
 val h_decompose_and   : constr -> tactic
 
-val double_ind : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis -> tactic
-val h_double_induction : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis->tactic
+val double_ind : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis -> tactic
+val h_double_induction : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis->tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0144fbb34..a2e76cd9e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -33,7 +33,7 @@ open Tacexpr
 open Tacticals
 open Tactics
 open Tacred
-open Rawterm
+open Glob_term
 open Coqlib
 open Vernacexpr
 open Declarations
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 304aa43ae..2cf4b3027 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -21,7 +21,7 @@ open Tacticals
 open Tactics
 open Tacexpr
 open Termops
-open Rawterm
+open Glob_term
 open Genarg
 open Ind_tables
 (*i*)
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 40b628315..044ec3d3b 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -11,7 +11,7 @@ open Names
 open Tacexpr
 open Termops
 
-val instantiate : int -> Tacinterp.interp_sign * Rawterm.glob_constr ->
+val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
   (identifier * hyp_location_flag, unit) location -> tactic
 
 (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index e31428f7c..6bdbdb80b 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -52,7 +52,7 @@ END
 
 let pr_int_list = pr_int_list_full () () ()
 
-open Rawterm
+open Glob_term
 
 let pr_occurrences _prc _prlc _prt l =
   match l with
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 66c251971..5f3a8e260 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -12,7 +12,7 @@ open Names
 open Proof_type
 open Topconstr
 open Termops
-open Rawterm
+open Glob_term
 
 val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
@@ -22,12 +22,12 @@ val pr_orient : bool -> Pp.std_ppcmds
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
-val pr_occurrences : int list Rawterm.or_var -> Pp.std_ppcmds
+val pr_occurrences : int list Glob_term.or_var -> Pp.std_ppcmds
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
 val wit_raw : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type
 val raw : constr_expr Pcoq.Gram.entry
-val pr_raw : (Tacinterp.interp_sign * Rawterm.glob_constr) -> Pp.std_ppcmds
+val pr_raw : (Tacinterp.interp_sign * Glob_term.glob_constr) -> Pp.std_ppcmds
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 9a9ef164e..6377eafd9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -15,7 +15,7 @@ open Extraargs
 open Mod_subst
 open Names
 open Tacexpr
-open Rawterm
+open Glob_term
 open Tactics
 open Util
 open Evd
@@ -324,11 +324,11 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c (Glob_term.RProp Term.Null) false inv_clear_tac ]
 END
 
 open Term
-open Rawterm
+open Glob_term
 
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
@@ -395,7 +395,7 @@ END
 open Tactics
 open Tactics
 open Libnames
-open Rawterm
+open Glob_term
 open Summary
 open Libobject
 open Lib
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 1c6d72e9e..a92330f17 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -10,7 +10,7 @@ open Term
 open Proof_type
 open Tacmach
 
-open Rawterm
+open Glob_term
 open Refiner
 open Genarg
 open Tacexpr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index dd2b0bf50..8c0092980 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -13,7 +13,7 @@ open Proof_type
 open Tacmach
 open Genarg
 open Tacexpr
-open Rawterm
+open Glob_term
 open Evd
 open Clenv
 open Termops
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 1d1ab3f9e..2ae4e22e5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -32,7 +32,7 @@ open Equality
 open Typing
 open Pattern
 open Matching
-open Rawterm
+open Glob_term
 open Genarg
 open Tacexpr
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index e4daa082f..ef828d882 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -12,7 +12,7 @@ open Term
 open Tacmach
 open Genarg
 open Tacexpr
-open Rawterm
+open Glob_term
 
 type inversion_status = Dep of constr option | NoDep
 
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index b4b5737b5..1ac9b4d6f 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -1,7 +1,7 @@
 open Util
 open Names
 open Term
-open Rawterm
+open Glob_term
 open Proof_type
 open Topconstr
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1faf9489b..188bc3dc5 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -26,7 +26,7 @@ open Tactics
 open Pattern
 open Clenv
 open Auto
-open Rawterm
+open Glob_term
 open Hiddentac
 open Typeclasses
 open Typeclasses_errors
@@ -1582,7 +1582,7 @@ let setoid_transitivity c gl =
       let proof = get_transitive_proof env evm car rel in
       match c with
       | None -> eapply proof
-      | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ]))
+      | Some c -> apply_with_bindings (proof,Glob_term.ImplicitBindings [ c ]))
     (transitivity_red true c)
 
 let setoid_symmetry_in id gl =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f193c537a..917a98c55 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -15,7 +15,7 @@ open Libobject
 open Pattern
 open Matching
 open Pp
-open Rawterm
+open Glob_term
 open Sign
 open Tacred
 open Util
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index ca5acad31..9d782bd41 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -99,8 +99,8 @@ val intern_constr :
   glob_sign -> constr_expr -> glob_constr_and_expr
 
 val intern_constr_with_bindings :
-  glob_sign -> constr_expr * constr_expr Rawterm.bindings ->
-  glob_constr_and_expr * glob_constr_and_expr Rawterm.bindings
+  glob_sign -> constr_expr * constr_expr Glob_term.bindings ->
+  glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings
 
 val intern_hyp :
   glob_sign -> identifier Util.located -> identifier Util.located
@@ -127,7 +127,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list ->
 
 val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
 
-val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings
+val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings
 
 (** Initial call for interpretation *)
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dc013fda6..2598cab5e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -21,7 +21,7 @@ open Refiner
 open Tacmach
 open Clenv
 open Clenvtac
-open Rawterm
+open Glob_term
 open Pattern
 open Matching
 open Genarg
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index b030a09c3..db9ab0c9b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -19,7 +19,7 @@ open Pattern
 open Genarg
 open Tacexpr
 open Termops
-open Rawterm
+open Glob_term
 
 (** Tacticals i.e. functions from tactics to tactics. *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c4201f99..11bb6b436 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -24,7 +24,7 @@ open Libnames
 open Evd
 open Pfedit
 open Tacred
-open Rawterm
+open Glob_term
 open Tacmach
 open Proof_type
 open Logic
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 136815368..a2dd6e411 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -23,7 +23,7 @@ open Libnames
 open Genarg
 open Tacexpr
 open Nametab
-open Rawterm
+open Glob_term
 open Pattern
 open Termops
 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 43b94f09a..443acc6f5 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -11,7 +11,7 @@ open Names
 open Nameops
 open Term
 open Pattern
-open Rawterm
+open Glob_term
 open Libnames
 open Nametab