Rebranchement de la tactique Let

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

1 files changed, 12 insertions, 1 deletions

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)
+