Problèmes et améliorations divers affichage

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

7 files changed, 61 insertions, 29 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index f26d0dc2ab..4373da4628 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -484,7 +484,7 @@ let abstract_path typ path t =
 
 let focused_simpl path gl =
   let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  convert_concl newc gl
+  convert_concl_no_check newc gl
 
 let focused_simpl path = simpl_time (focused_simpl path)
 
@@ -1723,13 +1723,13 @@ let destructure_hyps gl =
 		      match destructurate (pf_nf gl typ) with
 			| Kapp("nat",_) -> 
                                (tclTHEN 
-			       (convert_hyp
+			       (convert_hyp_no_check
                                   (i,body,
 				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
 			       (loop evbd lit))
 			| Kapp("Z",_) ->
                                (tclTHEN 
-			       (convert_hyp
+			       (convert_hyp_no_check
                                   (i,body,
 				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
 			       (loop evbd lit))
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index e6e7074aa8..75bc2d1b0f 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -574,7 +574,7 @@ let prepare_and_play env tac_hyps trace_solution =
     Pp.ppnl (Printer.prterm reified_trace_solution);
   end;
   Tactics.generalize l_generalized >>
-  Tactics.change_in_concl reified >>
+  Tactics.change_in_concl None reified >>
   Tacticals.tclTRY 
     (Tactics.apply (mkApp (Lazy.force coq_normalize_sequent, 
 			   [|l_reified_tac_norms |]))) >>
@@ -797,13 +797,13 @@ let destructure_hyps gl =
 		      match destructurate (pf_nf gl typ) with
 			| Kapp("nat",_) -> 
                             (tclTHEN 
-			       (convert_hyp
+			       (convert_hyp_no_check
                                   (i,body,
 				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
 			       (loop evbd lit))
 			| Kapp("Z",_) ->
                             (tclTHEN 
-			       (convert_hyp
+			       (convert_hyp_no_check
                                   (i,body,
 				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
 			       (loop evbd lit))
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9e86405cc1..4ecd57ba68 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -57,6 +57,8 @@ let print_universes = ref false
 (* This suppresses printing of numeral and symbols *)
 let print_no_symbol = ref false
 
+let print_meta_as_hole = ref false
+
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
@@ -67,6 +69,7 @@ let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
 let with_universes f = with_option print_universes f
 let without_symbols f = with_option print_no_symbol f
+let with_meta_as_hole f = with_option print_meta_as_hole f
 
 (**********************************************************************)
 (* Various externalisation functions *)
@@ -100,7 +103,22 @@ let idopt_of_name = function
 
 let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
 
-let extern_reference loc r = Qualid (loc,shortest_qualid_of_global None r)
+let raw_string_of_ref = function
+  | ConstRef kn -> 
+      "CONST("^(string_of_kn kn)^")"
+  | IndRef (kn,i) ->
+      "IND("^(string_of_kn kn)^","^(string_of_int i)^")"
+  | ConstructRef ((kn,i),j) -> 
+      "CONSTRUCT("^
+      (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")"
+  | VarRef id -> 
+      "SECVAR("^(string_of_id id)^")"
+
+let extern_reference loc r =
+  try Qualid (loc,shortest_qualid_of_global None r)
+  with Not_found ->
+    (* happens in debugger *)
+    Ident (loc,id_of_string (raw_string_of_ref r))
 
 (**********************************************************************)
 (* conversion of terms and cases patterns                             *)
@@ -192,7 +210,7 @@ let rec extern scopes r =
 
   | REvar (_,n) -> extern_evar loc n
 
-  | RMeta (_,n) -> CMeta (loc,n)
+  | RMeta (_,n) -> if !print_meta_as_hole then CHole loc else CMeta (loc,n)
 
   | RApp (_,f,args) ->
       let (f,args) =
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 98c500c122..713306690b 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -51,7 +51,7 @@ let ppcmd_of_cut = function
   | PpTbrk(n1,n2) -> tbrk(n1,n2)
 
 type unparsing = 
-  | UnpMetaVar of int * tolerability
+  | UnpMetaVar of tolerability
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 625c85e680..4d83eda3d2 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -41,7 +41,7 @@ val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
 val ppcmd_of_cut : ppcut -> std_ppcmds
 
 type unparsing = 
-  | UnpMetaVar of int * tolerability
+  | UnpMetaVar of tolerability
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 53c9453d0b..2758dcff48 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -259,7 +259,15 @@ let rec detype tenv avoid env t =
 	  RCases (dummy_loc,pred,[tomatch],eqnl)
 	else
 	  let bl = Array.map (detype tenv avoid env) bl in
-	  ROrderedCase (dummy_loc,LetStyle,pred,tomatch,bl)
+	  let rec remove_type n c = if n = 0 then c else
+	    match c with
+	      | RLambda (loc,na,t,c) ->
+		  let h = RHole (loc,AbstractionType na) in
+		  RLambda (loc,na,h,remove_type (n-1) c)
+	      | RLetIn (loc,na,b,c) -> RLetIn (loc,na,b,remove_type (n-1) c)
+	      | _ -> anomaly "Not a context" in
+	  let bl = array_map2 remove_type consnargsl bl in
+	  ROrderedCase (dummy_loc,tag,pred,tomatch,bl)
 	
     | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef
     | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7313ed7bd8..f408c07f48 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -276,11 +276,11 @@ let add_break l = function
   | _ -> l
 
 let precedence_of_entry_type = function
-  | ETConstr (n,BorderProd (left,None)) -> (n,Prec n)
+  | ETConstr (n,BorderProd (_,None)) -> n, Prec n
   | ETConstr (n,BorderProd (left,Some a)) ->
-      (n, let (lp,rp) = prec_assoc a in if left then lp else rp)
-  | ETConstr (n,InternalProd) -> (n,E)
-  | _ -> 0,E
+      n, let (lp,rp) = prec_assoc a in if left then lp else rp
+  | ETConstr (n,InternalProd) -> n, Prec n
+  | _ -> 0, E (* ?? *)
 
 (* x = y |-> x brk = y (breaks before any symbol) *)
 (* x =S y |-> x spc =S spc y (protect from confusion; each side for symmetry)*)
@@ -293,7 +293,7 @@ let make_hunks_ast symbols etyps from =
   List.fold_right
     (fun it (ws,l) -> match it with
       | NonTerminal m ->
-	  let (n,lp) = precedence_of_entry_type (List.assoc m etyps) in
+	  let _,lp = precedence_of_entry_type (List.assoc m etyps) in
 	  let u = PH (meta_pattern (string_of_id m), None, lp) in
 	  let l' = u :: (add_break l ws) in
 	  (Separate 1, l')
@@ -308,13 +308,17 @@ let make_hunks_ast symbols etyps from =
 		Separate 1,
 		if ws = Separate 0 then s^" ",l else s,add_break l ws
 	      else
-		Juxtapose, (s,l) in
+		Juxtapose, (s,add_break l ws) in
 	    (n, RO s :: l)
       | Break n ->
 	    (Juxtapose, UNP_BRK (n,1) :: l))
     symbols (Juxtapose,[])
   in l
 
+let add_break l = function
+  | Separate n -> UnpCut (PpBrk(n,1)) :: l
+  | _ -> l
+
 let make_hunks etyps symbols =
   let vars,typs = List.split etyps in
   let (_,l) =
@@ -322,21 +326,23 @@ let make_hunks etyps symbols =
     (fun it (ws,l) -> match it with
       | NonTerminal m ->
 	  let i = list_index m vars in
-	  let prec = precedence_of_entry_type (List.nth typs (i-1)) in
+	  let _,prec = precedence_of_entry_type (List.nth typs (i-1)) in
 	  let u = UnpMetaVar (i ,prec) in
-	  let l' = match ws with
-	    | Separate n -> UnpCut (PpBrk(n,1)) :: u :: l
-	    | _ -> u :: l in
+	  let l' = u :: (add_break l ws) in
 	  (Separate 1, l')
       | Terminal s ->
-	  let n = if is_letter (s.[0]) then 1 else 0 in
-	  let s = 
-	    if (ws = Separate 1)
-	      & is_letter (s.[String.length s -1])
-	    then s^" "
-	    else s
-	  in
-	  (Separate n, UnpTerminal s :: l)
+	    let n,(s,l) =
+	      if
+		is_letter (s.[0]) or 
+		is_letter (s.[String.length s -1]) or
+		is_digit (s.[String.length s -1])
+	      then
+		(* We want spaces around both sides *)
+		1, if ws = Separate 0 then s^" ",l else s,add_break l ws
+	      else
+		(* We want a break before symbols, hence [Separate 0] *)
+		0, (s,l) in
+	    (Separate n, UnpTerminal s :: l)
       | Break n ->
 	    (Juxtapose, UnpCut (PpBrk (n,1)) :: l))
     symbols (Juxtapose,[])