Change of nomenclature: rawconstr -> glob_constr

There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.

In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.

The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.

This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):

perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`

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

7 files changed, 73 insertions, 73 deletions

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index d9addd1f05..e1e04c8eff 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -290,7 +290,7 @@ let applyDestructor cls discard dd gls =
       match cl, dd.d_code with
         | Some id, (Some x, tac) ->
 	    let arg =
-              ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
+              ConstrMayEval(ConstrTerm (GRef(dummy_loc,VarRef id),None)) in
             TacLetIn (false, [(dummy_loc, x), arg], tac)
         | None, (None, tac) -> tac
         | _, (Some _,_) -> error "Destructor expects an hypothesis."
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index dc8168ca89..40b628315b 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.rawconstr ->
+val instantiate : int -> Tacinterp.interp_sign * Rawterm.glob_constr ->
   (identifier * hyp_location_flag, unit) location -> tactic
 
 (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 25a64c3dd5..e31428f7c1 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -103,17 +103,17 @@ let pr_occurrences = pr_occurrences () () ()
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_glob_constr raw
 let pr_raw = pr_rawc () () ()
 
 let interp_raw ist gl (t,_) = (ist,t)
 
 let glob_raw = Tacinterp.intern_constr
 
-let subst_raw = Tacinterp.subst_rawconstr_and_expr
+let subst_raw = Tacinterp.subst_glob_constr_and_expr
 
 ARGUMENT EXTEND raw
-    TYPED AS rawconstr
+    TYPED AS glob_constr
     PRINTED BY pr_rawc
 
      INTERPRETED BY interp_raw
@@ -123,7 +123,7 @@ ARGUMENT EXTEND raw
      RAW_TYPED AS constr_expr
      RAW_PRINTED BY pr_gen
 
-     GLOB_TYPED AS rawconstr_and_expr
+     GLOB_TYPED AS glob_constr_and_expr
      GLOB_PRINTED BY pr_gen
   [ lconstr(c) ] -> [ c ]
 END
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index f276426789..66c251971e 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -25,9 +25,9 @@ val wit_occurrences : (int list) typed_abstract_argument_type
 val pr_occurrences : int list Rawterm.or_var -> Pp.std_ppcmds
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_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.rawconstr) -> Pp.std_ppcmds
+val pr_raw : (Tacinterp.interp_sign * Rawterm.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 78a1f51b78..9a9ef164ed 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -540,12 +540,12 @@ let subst_var_with_hole occ tid t =
   let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec = function
-    | RVar (_,id) as x -> 
+    | GVar (_,id) as x -> 
         if id = tid 
         then (decr occref; if !occref = 0 then x
-                           else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
+                           else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
         else x
-    | c -> map_rawconstr_left_to_right substrec c in
+    | c -> map_glob_constr_left_to_right substrec c in
   let t' = substrec t
   in
   if !occref > 0 then Termops.error_invalid_occurrence [occ] else t'
@@ -554,10 +554,10 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | RHole (_,Evd.QuestionMark(Evd.Define true)) -> 
+    | GHole (_,Evd.QuestionMark(Evd.Define true)) -> 
         decr occref; if !occref = 0 then tc
-                     else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
-    | c -> map_rawconstr_left_to_right substrec c
+                     else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
+    | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d4ac859ad8..f193c537a2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -371,12 +371,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict & find_hyp id ist ->
-      RVar (dloc,id), Some (CRef r)
+      GVar (dloc,id), Some (CRef r)
   | Ident (_,id) as r when find_ctxvar id ist ->
-      RVar (dloc,id), if strict then None else Some (CRef r)
+      GVar (dloc,id), if strict then None else Some (CRef r)
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
+      GRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
 
 let intern_move_location ist = function
   | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id)
@@ -502,7 +502,7 @@ let intern_induction_arg ist = function
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
 	match intern_constr ist (CRef (Ident (dloc,id))) with
-	| RVar (loc,id),_ -> ElimOnIdent (loc,id)
+	| GVar (loc,id),_ -> ElimOnIdent (loc,id)
 	| c -> ElimOnConstr (c,NoBindings)
       else
 	ElimOnIdent (loc,id)
@@ -555,7 +555,7 @@ let intern_typed_pattern ist p =
   let dummy_pat = PRel 0 in
   (* we cannot ensure in non strict mode that the pattern is closed *)
   (* keeping a constr_expr copy is too complicated and we want anyway to *)
-  (* type it, so we remember the pattern as a rawconstr only *)
+  (* type it, so we remember the pattern as a glob_constr only *)
   (intern_constr_gen true false ist p,dummy_pat)
 
 let intern_typed_pattern_with_occurrences ist (l,p) =
@@ -870,7 +870,7 @@ and intern_tacarg strict ist = function
       let id = id_of_string s in
       if find_ltacvar id ist then
 	if istac then Reference (ArgVar (adjust_loc loc,id))
-	else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
+	else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None))
       else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
   | TacCall (loc,f,l) ->
@@ -1332,7 +1332,7 @@ let constr_list_of_VList env = function
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
-    | RVar (_,id), _ ->	
+    | GVar (_,id), _ ->	
         sigma,
         List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun))
     | _ ->
@@ -1417,7 +1417,7 @@ let interp_may_eval f ist gl = function
 	f ist gl c
      with e ->
        debugging_exception_step ist false e (fun () ->
-         str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c));
+         str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
        raise e
 
 (* Interprets a constr expression possibly to first evaluate *)
@@ -1553,11 +1553,11 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
 
 let loc_of_bindings = function
 | NoBindings -> dummy_loc
-| ImplicitBindings l -> loc_of_rawconstr (fst (list_last l))
+| ImplicitBindings l -> loc_of_glob_constr (fst (list_last l))
 | ExplicitBindings l -> pi1 (list_last l)
 
 let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
-  let loc1 = loc_of_rawconstr c in
+  let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
   let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in
   let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
@@ -1594,7 +1594,7 @@ let interp_induction_arg ist gl sigma arg =
 	if Tactics.is_quantified_hypothesis id gl then
           sigma, ElimOnIdent (loc,id)
 	else
-          let c = (RVar (loc,id),Some (CRef (Ident (loc,id)))) in
+          let c = (GVar (loc,id),Some (CRef (Ident (loc,id)))) in
           let c = interp_constr ist env sigma c in
           sigma, ElimOnConstr (c,NoBindings)
 
@@ -2068,7 +2068,7 @@ and interp_genarg ist gl x =
       in_gen wit_sort
         (destSort
 	  (pf_interp_constr ist gl
-	    (RSort (dloc,out_gen globwit_sort x), None)))
+	    (GSort (dloc,out_gen globwit_sort x), None)))
   | ConstrArgType ->
       in_gen wit_constr (pf_interp_constr ist gl (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
@@ -2539,22 +2539,22 @@ let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
 
-let subst_rawconstr_and_expr subst (c,e) =
+let subst_glob_constr_and_expr subst (c,e) =
   assert (e=None); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_rawconstr subst c,None)
+  (Detyping.subst_glob_constr subst c,None)
 
-let subst_rawconstr = subst_rawconstr_and_expr (* shortening *)
+let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
 let subst_binding subst (loc,b,c) =
-  (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)
+  (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c)
 
 let subst_bindings subst = function
   | NoBindings -> NoBindings
-  | ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l)
+  | ImplicitBindings l -> ImplicitBindings (List.map (subst_glob_constr subst) l)
   | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)
 
 let subst_raw_with_bindings subst (c,bl) =
-  (subst_rawconstr subst c, subst_bindings subst bl)
+  (subst_glob_constr subst c, subst_bindings subst bl)
 
 let subst_induction_arg subst = function
   | ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c)
@@ -2598,17 +2598,17 @@ let subst_unfold subst (l,e) =
 let subst_flag subst red =
   { red with rConst = List.map (subst_evaluable subst) red.rConst }
 
-let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c)
+let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
-let subst_rawconstr_or_pattern subst (c,p) =
-  (subst_rawconstr subst c,subst_pattern subst p)
+let subst_glob_constr_or_pattern subst (c,p) =
+  (subst_glob_constr subst c,subst_pattern subst p)
 
 let subst_pattern_with_occurrences subst (l,p) =
-  (l,subst_rawconstr_or_pattern subst p)
+  (l,subst_glob_constr_or_pattern subst p)
 
 let subst_redexp subst = function
   | Unfold l -> Unfold (List.map (subst_unfold subst) l)
-  | Fold l -> Fold (List.map (subst_rawconstr subst) l)
+  | Fold l -> Fold (List.map (subst_glob_constr subst) l)
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
@@ -2616,14 +2616,14 @@ let subst_redexp subst = function
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
-  | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
-  | ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c)
-  | ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c)
-  | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
+  | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)
+  | ConstrContext (locid,c) -> ConstrContext (locid,subst_glob_constr subst c)
+  | ConstrTypeOf c -> ConstrTypeOf (subst_glob_constr subst c)
+  | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_rawconstr_or_pattern subst pc))
-  | Term pc -> Term (subst_rawconstr_or_pattern subst pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc))
+  | Term pc -> Term (subst_glob_constr_or_pattern subst pc)
 
 let rec subst_match_goal_hyps subst = function
   | Hyp (locs,mp) :: tl ->
@@ -2638,39 +2638,39 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
   | TacAssumption as x -> x
-  | TacExact c -> TacExact (subst_rawconstr subst c)
-  | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
-  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
+  | TacExact c -> TacExact (subst_glob_constr subst c)
+  | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,subst_raw_with_bindings subst cb,
                Option.map (subst_raw_with_bindings subst) cbo)
-  | TacElimType c -> TacElimType (subst_rawconstr subst c)
+  | TacElimType c -> TacElimType (subst_glob_constr subst c)
   | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
-  | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
+  | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
   | TacFix (idopt,n) as x -> x
   | TacMutualFix (b,id,n,l) ->
-      TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+      TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
   | TacCofix idopt as x -> x
   | TacMutualCofix (b,id,l) ->
-      TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
-  | TacCut c -> TacCut (subst_rawconstr subst c)
+      TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
+  | TacCut c -> TacCut (subst_glob_constr subst c)
   | TacAssert (b,na,c) ->
-      TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
+      TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
-  | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
-  | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b)
+  | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
+  | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
 
   (* Automation tactics *)
-  | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
-  | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)
+  | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l)
+  | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
-  | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems)
+  | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems)
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) as x -> x
@@ -2679,13 +2679,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 	List.map (subst_induction_arg subst) lc,
         Option.map (subst_raw_with_bindings subst) cbo, ids) l, cls))
   | TacDoubleInduction (h1,h2) as x -> x
-  | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
-  | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
+  | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
+  | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
   | TacDecompose (l,c) ->
       let l = List.map (subst_or_var (subst_inductive subst)) l in
-      TacDecompose (l,subst_rawconstr subst c)
+      TacDecompose (l,subst_glob_constr subst c)
   | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l)
-  | TacLApply c -> TacLApply (subst_rawconstr subst c)
+  | TacLApply c -> TacLApply (subst_glob_constr subst c)
 
   (* Context management *)
   | TacClear _ as x -> x
@@ -2704,12 +2704,12 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (op,c,cl) ->
-      TacChange (Option.map (subst_rawconstr_or_pattern subst) op,
-        subst_rawconstr subst c, cl)
+      TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+        subst_glob_constr subst c, cl)
 
   (* Equivalence relations *)
   | TacReflexivity | TacSymmetry _ as x -> x
-  | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c)
+  | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
@@ -2718,10 +2718,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 			      b,m,subst_raw_with_bindings subst c) l,
 		 cl,Option.map (subst_tactic subst) by)
   | TacInversion (DepInversion (k,c,l),hyp) ->
-     TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
+     TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
   | TacInversion (InversionUsing (c,cl),hyp) ->
-      TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
+      TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
 
   (* For extensions *)
   | TacExtend (_loc,opn,l) ->
@@ -2808,7 +2808,7 @@ and subst_genarg subst (x:glob_generic_argument) =
   | SortArgType ->
       in_gen globwit_sort (out_gen globwit_sort x)
   | ConstrArgType ->
-      in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x))
+      in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
       in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
   | QuantHypArgType ->
@@ -2819,7 +2819,7 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
-        ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
+        ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index ee3401a08c..ca5acad318 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -96,11 +96,11 @@ val intern_tactic :
   glob_sign -> raw_tactic_expr -> glob_tactic_expr
 
 val intern_constr :
-  glob_sign -> constr_expr -> rawconstr_and_expr
+  glob_sign -> constr_expr -> glob_constr_and_expr
 
 val intern_constr_with_bindings :
   glob_sign -> constr_expr * constr_expr Rawterm.bindings ->
-  rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings
+  glob_constr_and_expr * glob_constr_and_expr Rawterm.bindings
 
 val intern_hyp :
   glob_sign -> identifier Util.located -> identifier Util.located
@@ -108,8 +108,8 @@ val intern_hyp :
 val subst_genarg :
   substitution -> glob_generic_argument -> glob_generic_argument
 
-val subst_rawconstr_and_expr :
-  substitution -> rawconstr_and_expr -> rawconstr_and_expr
+val subst_glob_constr_and_expr :
+  substitution -> glob_constr_and_expr -> glob_constr_and_expr
 
 (** Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
@@ -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 -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings
+val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings
 
 (** Initial call for interpretation *)
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr