Standardisation du nom de subst_raw en subst_rawconstr

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

3 files changed, 32 insertions, 28 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0d3e6674ec..5b26eaec5f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -459,16 +459,16 @@ and detype_binder isgoal bk avoid env na ty c =
     | BLambda -> RLambda (dummy_loc, na',detype isgoal avoid env ty, r)
     | BLetIn -> RLetIn (dummy_loc, na',detype isgoal avoid env ty, r)
 
-let rec subst_pat subst pat = 
+let rec subst_cases_pattern subst pat = 
   match pat with
   | PatVar _ -> pat
   | PatCstr (loc,((kn,i),j),cpl,n) -> 
       let kn' = subst_kn subst kn 
-      and cpl' = list_smartmap (subst_pat subst) cpl in
+      and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 
-let rec subst_raw subst raw = 
+let rec subst_rawconstr subst raw = 
   match raw with
   | RRef (loc,ref) -> 
       let ref',t = subst_global subst ref in 
@@ -480,30 +480,30 @@ let rec subst_raw subst raw =
   | RPatVar _ -> raw
 
   | RApp (loc,r,rl) -> 
-      let r' = subst_raw subst r 
-      and rl' = list_smartmap (subst_raw subst) rl in
+      let r' = subst_rawconstr subst r 
+      and rl' = list_smartmap (subst_rawconstr subst) rl in
 	if r' == r && rl' == rl then raw else
 	  RApp(loc,r',rl')
 
   | RLambda (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  RLambda (loc,n,r1',r2')
 
   | RProd (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  RProd (loc,n,r1',r2')
 
   | RLetIn (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
   | RCases (loc,rtno,rl,branches) -> 
-      let rtno' = option_smartmap (subst_raw subst) rtno
+      let rtno' = option_smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
-        let a' = subst_raw subst a in
+        let a' = subst_rawconstr subst a in
         let (n,topt) = x in 
         let topt' = option_smartmap
           (fun (loc,(sp,i),x as t) ->
@@ -512,8 +512,9 @@ let rec subst_raw subst raw =
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap 
 			(fun (loc,idl,cpl,r as branch) ->
-			   let cpl' = list_smartmap (subst_pat subst) cpl
-			   and r' = subst_raw subst r in
+			   let cpl' =
+			     list_smartmap (subst_cases_pattern subst) cpl
+			   and r' = subst_rawconstr subst r in
 			     if cpl' == cpl && r' == r then branch else
 			       (loc,idl,cpl',r'))
 			branches
@@ -522,27 +523,27 @@ let rec subst_raw subst raw =
 	  RCases (loc,rtno',rl',branches')
 
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_raw subst) po
-      and b' = subst_raw subst b 
-      and c' = subst_raw subst c in
+      let po' = option_smartmap (subst_rawconstr subst) po
+      and b' = subst_rawconstr subst b 
+      and c' = subst_rawconstr subst c in
 	if po' == po && b' == b && c' == c then raw else
           RLetTuple (loc,nal,(na,po'),b',c')
       
   | RIf (loc,c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_raw subst) po
-      and b1' = subst_raw subst b1 
-      and b2' = subst_raw subst b2 
-      and c' = subst_raw subst c in
+      let po' = option_smartmap (subst_rawconstr subst) po
+      and b1' = subst_rawconstr subst b1 
+      and b2' = subst_rawconstr subst b2 
+      and c' = subst_rawconstr subst c in
 	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
           RIf (loc,c',(na,po'),b1',b2')
 
   | RRec (loc,fix,ida,bl,ra1,ra2) -> 
-      let ra1' = array_smartmap (subst_raw subst) ra1
-      and ra2' = array_smartmap (subst_raw subst) ra2 in
+      let ra1' = array_smartmap (subst_rawconstr subst) ra1
+      and ra2' = array_smartmap (subst_rawconstr subst) ra2 in
       let bl' = array_smartmap
         (list_smartmap (fun (na,obd,ty as dcl) ->
-          let ty' = subst_raw subst ty in
-          let obd' = option_smartmap (subst_raw subst) obd in
+          let ty' = subst_rawconstr subst ty in
+          let obd' = option_smartmap (subst_rawconstr subst) obd in
           if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
@@ -558,9 +559,8 @@ let rec subst_raw subst raw =
       InternalHole | TomatchTypeParameter _)) -> raw
 
   | RCast (loc,r1,k,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  RCast (loc,r1',k,r2')
 
   | RDynamic _ -> raw
-
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 00b7c471a1..2a16b9e7ee 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -19,7 +19,9 @@ open Termops
 open Mod_subst
 (*i*)
 
-val subst_raw : substitution -> rawconstr -> rawconstr
+val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
+
+val subst_rawconstr : substitution -> rawconstr -> rawconstr
 
 (* [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr *)
 (* de Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6c7be7d288..2442b4aa5b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1869,9 +1869,11 @@ let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
 
-let subst_rawconstr subst (c,e) =
+let subst_rawconstr_and_expr subst (c,e) =
   assert (e=None); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_raw subst c,None)
+  (Detyping.subst_rawconstr subst c,None)
+
+let subst_rawconstr = subst_rawconstr_and_expr (* shortening *)
 
 let subst_binding subst (loc,b,c) =
   (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)