Nouveau Rewrite-in plus economique

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

3 files changed, 9 insertions, 18 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 719205331c..79900a84ef 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -43,9 +43,6 @@ val type_of_constructor  : env -> constructor -> types
 (* Return constructor types in normal form *)
 val arities_of_constructors : env -> inductive -> types array
 
-
-exception Arity of (constr * constr * Type_errors.arity_error) option
-
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
diff --git a/kernel/term.ml b/kernel/term.ml
index 16524ea469..62f21de5fc 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -644,15 +644,14 @@ let map_rel_declaration = map_named_declaration
 (*     Occurring     *)
 (*********************)
 
-exception FreeVar
-exception Occur
+exception LocalOccur
 
 (* (closedn n M) raises FreeVar if a variable of height greater than n
    occurs in M, returns () otherwise *)
 
 let closedn = 
   let rec closed_rec n c = match kind_of_term c with
-    | Rel m -> if m>n then raise FreeVar
+    | Rel m -> if m>n then raise LocalOccur
     | _ -> iter_constr_with_binders succ closed_rec n c
   in 
   closed_rec
@@ -660,26 +659,26 @@ let closedn =
 (* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
 
 let closed0 term =
-  try closedn 0 term; true with FreeVar -> false
+  try closedn 0 term; true with LocalOccur -> false
 
 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
 
 let noccurn n term = 
   let rec occur_rec n c = match kind_of_term c with
-    | Rel m -> if m = n then raise Occur
+    | Rel m -> if m = n then raise LocalOccur
     | _ -> iter_constr_with_binders succ occur_rec n c
   in 
-  try occur_rec n term; true with Occur -> false
+  try occur_rec n term; true with LocalOccur -> false
 
 (* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M 
   for n <= p < n+m *)
 
 let noccur_between n m term = 
   let rec occur_rec n c = match kind_of_term c with
-    | Rel(p) -> if n<=p && p<n+m then raise Occur
+    | Rel(p) -> if n<=p && p<n+m then raise LocalOccur
     | _        -> iter_constr_with_binders succ occur_rec n c
   in 
-  try occur_rec n term; true with Occur -> false
+  try occur_rec n term; true with LocalOccur -> false
 
 (* Checking function for terms containing existential variables.
  The function [noccur_with_meta] considers the fact that
@@ -690,7 +689,7 @@ let noccur_between n m term =
 
 let noccur_with_meta n m term = 
   let rec occur_rec n c = match kind_of_term c with
-    | Rel p -> if n<=p & p<n+m then raise Occur
+    | Rel p -> if n<=p & p<n+m then raise LocalOccur
     | App(f,cl) ->
 	(match kind_of_term f with
            | Cast (c,_) when isMeta c -> ()
@@ -699,7 +698,7 @@ let noccur_with_meta n m term =
     | Evar (_, _) -> ()
     | _ -> iter_constr_with_binders succ occur_rec n c
   in
-  try (occur_rec n term; true) with Occur -> false
+  try (occur_rec n term; true) with LocalOccur -> false
 
 
 (*********************)
@@ -720,8 +719,6 @@ let liftn k n =
  
 let lift k = liftn k 1
 
-let pop t = lift (-1) t
-
 (*********************)
 (*   Substituting    *)
 (*********************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 00f835e0d5..73f29ddbe5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -418,9 +418,6 @@ val liftn : int -> int -> constr -> constr
 (* [lift n c] lifts by [n] the positive indexes in [c] *)
 val lift : int -> constr -> constr
 
-(* [pop c] lifts by -1 the positive indexes in [c] *)
-val pop : constr -> constr
-
 (* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
     accordingly indexes in [a1],...,[an] *)