Rebranchement de la tactique Let

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

2 files changed, 16 insertions, 13 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2487d9160..aebc76539 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -188,16 +188,11 @@ let split_sign hfrom hto l =
   in 
   splitrec [] false l
 
-let occur_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
-
 let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
     if toleft
-    then occur_decl hyp2 d
-    else occur_decl hyp d2
+    then occur_var_in_decl hyp2 d
+    else occur_var_in_decl hyp d2
   in
   let rec moverec first middle = function
     | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
@@ -249,11 +244,8 @@ let check_backward_dependencies env d =
 
 let check_forward_dependencies id tail =
   List.iter
-    (function (id',c,t) ->
-       let b = match c with
-	 | None -> occur_var id (body_of_type t)
-	 | Some body -> occur_var id (body_of_type t) || occur_var id body in
-       if b then
+    (function (id',_,_ as decl) ->
+       if occur_var_in_decl id decl then
 	 error ((string_of_id id) ^ " is used in the hypothesis " 
 		^ (string_of_id id')))
     tail
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 30e5aeba2..2f7d069a8 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -371,4 +371,15 @@ let ast_of_cvt_arg = function
   | Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id)); 
                                           (ope ("COMMAND",[c]))])
   | Intropattern p ->  ast_of_cvt_intro_pattern p
-  | Letpatterns _ -> failwith "TODO: ast_of_cvt_arg: Letpatterns"
+  | Letpatterns (gl_occ_opt,hyp_occ_list) ->
+     let hyps_pats =
+       List.map
+	 (fun (id,l) ->
+	    ope ("HYPPATTERN", nvar (string_of_id id) :: (List.map num l)))
+	 hyp_occ_list in
+     let all_pats =
+       match gl_occ_opt with
+	 | None -> hyps_pats
+	 | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in
+     ope ("LETPATTERNS", all_pats)
+