Bug et améliorations diverses

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

2 files changed, 19 insertions, 4 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 29f3c437c5..97e9855de8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -125,8 +125,13 @@ let translate_keyword = function
     | "if"  | "then" | "else" | "return" as s) ->
       let s' = s^"_" in
       msgerrnl
-      (str ("Warning: "^s^" is now a keyword; it has been translated to "^s'));
+      (str ("Warning: '"^
+          s^"' is now a keyword; it has been translated to '"^s'^"'"));
       s'
+  | "_" -> 
+      msgerrnl (str 
+	"Warning: '_' is no longer a keyword; it has been translated to 'xx'");
+      "xx"
   | s -> s
 
 let is_coq_root d =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e86d60c77a..ffbca83eac 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -673,7 +673,8 @@ let rec pretype tycon env isevars lvar = function
           let nconstr = Array.length mip.mind_consnames in
           let tyi = snd ind in
           if isrec && mis_is_recursive_subset [tyi] recargs then
-            Some (Detyping.detype env [] (names_of_rel_context env)
+            Some (Detyping.detype env 
+	      (ids_of_context env) (names_of_rel_context env)
               (nf_evar (evars_of isevars) v))
   (*
             let sigma = evars_of isevars in
@@ -732,7 +733,12 @@ let rec pretype tycon env isevars lvar = function
               RApp (dummy_loc,fix,realargs@[c])
               (msgerrnl (str "Warning: could't translate Match"); None)
 *)
-          else
+          else if st = IfStyle & po = None then
+	    (* Translate into a "if ... then ... else" *)
+	    (* TODO: translate into a "if" even if po is dependent *)
+	    None
+	  else
+	    (* Translate into a "match ... with" *)
             let rtntypopt, indnalopt = match po with
               | None -> None, (Anonymous,None)
               | Some p ->
@@ -756,7 +762,11 @@ let rec pretype tycon env isevars lvar = function
                     else [Anonymous],p,[] in
                   let args = List.map (fun _ -> Anonymous) params @ nal in
                   (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in
-
+	    if st = IfStyle & po = None then
+	      (* Translate into a "if ... then ... else" *)
+	      (* TODO: translate into a "if" even if po is dependent *)
+	      None
+	    else
             let detype_eqn constr construct_nargs branch =
               let name_cons = function 
                 | Anonymous -> fun l -> l