Heuristique pour traduire if-then-else quand le re-typage echoue

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

1 files changed, 14 insertions, 0 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7657ce445..a7eb7d29a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1605,6 +1605,20 @@ let rec extern inctx scopes vars r =
   | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) ->
       extern false scopes vars x
 
+  | ROrderedCase (loc,IfStyle,typopt,tm,bv,_) when Options.do_translate () ->
+      let rec strip_branches = function
+        | (RLambda (_,_,_,c1), RLambda (_,_,_,c2)) -> strip_branches (c1,c2)
+        | x -> x in
+      let c1,c2 = strip_branches (bv.(0),bv.(1)) in
+      msgerrnl (str "Warning: unable to ensure the correctness of the translation of an if-then-else");
+      let bv = Array.map (sub_extern (typopt<>None) scopes vars) [|c1;c2|] in
+      COrderedCase
+	(loc,IfStyle,option_app (extern_type scopes vars) typopt,
+         sub_extern false scopes vars tm,Array.to_list bv)
+      (* We failed type-checking If and to translate it to CIf *)
+      (* try to remove the dependances in branches anyway *)
+
+
   | ROrderedCase (loc,cs,typopt,tm,bv,_) ->
       let bv = Array.map (sub_extern (typopt<>None) scopes vars) bv in
       COrderedCase