Deplacement subst_rawconstr dans Rawterm

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

5 files changed, 35 insertions, 34 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a79c2a523c..c240613ae5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -582,37 +582,6 @@ let extract_rhs pb =
 
 (**********************************************************************)
 (* Functions to deal with matrix factorization *)
-let occur_rawconstr id =
-  let rec occur = function
-    | RVar (loc,id') -> id = id'
-    | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
-    | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
-    | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
-    | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,(tyopt,rtntypopt),tml,pl) ->
-	(occur_option tyopt) or (occur_option !rtntypopt)
-        or (List.exists (fun (tm,_) -> occur tm) tml)
-	or (List.exists occur_pattern pl)
-    | ROrderedCase (loc,b,tyopt,tm,bv,_) -> 
-	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
-    | RLetTuple (loc,nal,rtntyp,b,c) -> 
-	occur_return_type rtntyp id
-        or (occur b) or (not (List.mem (Name id) nal) & (occur c))
-    | RIf (loc,c,rtntyp,b1,b2) -> 
-	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
-    | RRec (loc,fk,idl,tyl,bv) ->
-	(array_exists occur tyl) or
-	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
-    | RCast (loc,c,t) -> (occur c) or (occur t)
-    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
-
-  and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
-
-  and occur_option = function None -> false | Some p -> occur p
-
-  and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
-
-  in occur
 
 let occur_in_rhs na rhs =
   match na with
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 1c4e6b92cd..e05061f420 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -41,8 +41,6 @@ type ml_case_error =
 
 exception NotInferable of ml_case_error
 
-val occur_rawconstr : identifier -> rawconstr -> bool
-
 val pred_case_ml : (* raises [NotInferable] if not inferable *)
   env -> evar_map -> bool -> inductive_type -> int * types -> constr 
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 76967cb05b..e8965659e7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -525,7 +525,7 @@ let rec pretype tycon env isevars lvar = function
                 if List.for_all
                   (function
                     | Anonymous -> true
-                    | Name id -> not (Cases.occur_rawconstr id rtntyp)) nal
+                    | Name id -> not (occur_rawconstr id rtntyp)) nal
                 then (* No dependency in realargs *)
                   None
                 else
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index a1eb589ff3..f11caa566e 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -158,6 +158,38 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
+let occur_rawconstr id =
+  let rec occur = function
+    | RVar (loc,id') -> id = id'
+    | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
+    | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
+    | RCases (loc,(tyopt,rtntypopt),tml,pl) ->
+	(occur_option tyopt) or (occur_option !rtntypopt)
+        or (List.exists (fun (tm,_) -> occur tm) tml)
+	or (List.exists occur_pattern pl)
+    | ROrderedCase (loc,b,tyopt,tm,bv,_) -> 
+	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
+    | RLetTuple (loc,nal,rtntyp,b,c) -> 
+	occur_return_type rtntyp id
+        or (occur b) or (not (List.mem (Name id) nal) & (occur c))
+    | RIf (loc,c,rtntyp,b1,b2) -> 
+	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
+    | RRec (loc,fk,idl,tyl,bv) ->
+	(array_exists occur tyl) or
+	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
+    | RCast (loc,c,t) -> (occur c) or (occur t)
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
+
+  and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
+
+  and occur_option = function None -> false | Some p -> occur p
+
+  and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
+
+  in occur
+
 let rec subst_pat subst pat = 
   match pat with
   | PatVar _ -> pat
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2718cf9bbc..993b7e84a2 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -103,6 +103,8 @@ val map_rawconstr_with_binders_loc : loc ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
 *)
 
+val occur_rawconstr : identifier -> rawconstr -> bool
+
 val loc_of_rawconstr : rawconstr -> loc
 
 val subst_raw : Names.substitution -> rawconstr -> rawconstr