Rebranchement de la tactique Let

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

6 files changed, 24 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 100db950f0..0c6167a15c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -88,6 +88,9 @@ let fold_var_context f env a =
 	 (fun d (env,e) -> (push_var d env, f env d e))
          (var_context env) (reset_context env,a))
 
+let fold_var_context_reverse f a env =
+  Sign.fold_var_context_reverse f a (var_context env) 
+
 let process_var_context f env =
   Sign.fold_var_context
     (fun d env -> f env d) (var_context env) (reset_context env)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 42d560ec90..dc733b3b44 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -56,6 +56,9 @@ val map_context : (constr -> constr) -> env -> env
 val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
 val process_var_context : (env -> var_declaration -> env) -> env -> env
 
+(* Recurrence on [var_context] starting from younger decl *)
+val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> env -> 'a
+
 (* [process_var_context_both_sides f env] iters [f] on the var
    declarations of [env] taking as argument both the initial segment, the
    middle value and the tail segment *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 27aa150e62..d9438eb98a 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -43,6 +43,7 @@ let rec mem_var_context id = function
   | _ :: sign -> mem_var_context id sign
   | [] -> false
 let fold_var_context = List.fold_right
+let fold_var_context_reverse = List.fold_left
 let fold_var_context_both_sides = list_fold_right_and_left
 let it_var_context_quantifier f = List.fold_left (fun c d -> f d c)
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index bb2e083de7..30e1dae28d 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -25,6 +25,7 @@ val ids_of_var_context : var_context -> identifier list
 val map_var_context : (constr -> constr) -> var_context -> var_context
 val mem_var_context : identifier -> var_context -> bool
 val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> 'a
 val fold_var_context_both_sides :
   ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
 val it_var_context_quantifier :
diff --git a/kernel/term.ml b/kernel/term.ml
index 9829c1154f..9e3ed34797 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -957,6 +957,12 @@ let substl laml =
   substn_many (Array.map make_substituend (Array.of_list laml)) 0
 let subst1 lam = substl [lam]
 
+let substl_decl laml (id,bodyopt,typ as d) =
+  match bodyopt with
+    | None -> (id,None,substl laml typ)
+    | Some body -> (id, Some (substl laml body), typed_app (substl laml) typ)
+let subst1_decl lam = substl_decl [lam]
+
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
@@ -1425,6 +1431,11 @@ let occur_var s c =
   in 
   try occur_rec c; false with Occur -> true
 
+let occur_var_in_decl hyp (_,c,typ) =
+  match c with
+    | None -> occur_var hyp (body_of_type typ)
+    | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body
+
 (***************************************)
 (*  alpha and eta conversion functions *)                         
 (***************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index fe26462dec..7bba6d924e 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -478,6 +478,9 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
+val substl_decl : constr list -> var_declaration -> var_declaration
+val subst1_decl : constr -> var_declaration -> var_declaration
+
 (* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
 val global_vars : constr -> identifier list
 
@@ -526,6 +529,8 @@ val occur_evar : existential_key -> constr -> bool
    in c, [false] otherwise *)
 val occur_var : identifier -> constr -> bool
 
+val occur_var_in_decl : identifier -> var_declaration -> bool
+
 (* [dependent M N] is true iff M is eq\_constr with a subterm of N 
    M is appropriately lifted through abstractions of N *)
 val dependent : constr -> constr -> bool