petits changements de syntaxe

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

3 files changed, 39 insertions, 31 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 6177f1a969..0154110e55 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -418,7 +418,7 @@ let rec pr inherited a =
 	str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
         str " =>" ++ spc() ++ pr ltop a),
       llambda
-  | CLetIn (_,(_,Name x),(CFix(_,(_,x'),_)|CCoFix(_,(_,x'),_) as fx), b)
+  | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
       hv 0 (
         hov 2 (str "let " ++ pr ltop fx ++ str " in") ++
@@ -600,8 +600,15 @@ let pr_lrawconstr_env env c =
 
 let pr_cases_pattern = pr_patt ltop
 
-let pr_occurrences prc (nl,c) =
-   prc c ++ prlist (fun n -> spc () ++ int n) nl
+let pr_pattern_occ prc = function
+    ([],c) -> prc c
+  | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
+                     hov 0 (prlist_with_sep spc int nl))
+
+let pr_unfold_occ pr_ref = function
+    ([],qid) -> pr_ref qid
+  | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
+                       hov 0 (prlist_with_sep spc int nl))
 
 let pr_qualid qid = str (string_of_qualid qid)
 
@@ -627,7 +634,7 @@ let pr_metaid id = str"?" ++ pr_id id
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_constr) o  
+  | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o  
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -636,13 +643,12 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Lazy f -> 
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
-      hov 1 (str "unfold " ++
-        prlist_with_sep pr_coma (fun (nl,qid) ->
-	  pr_ref qid ++ prlist (pr_arg int) nl) l)
+      hov 1 (str "unfold" ++ spc() ++
+             prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
       hov 1 (str "pattern" ++
-        pr_arg (prlist_with_sep pr_coma (pr_occurrences pr_constr)) l)
+        pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr (s,c) ->
@@ -656,10 +662,10 @@ let rec pr_may_eval prc prlc pr2 = function
 	 str " in" ++ spc() ++ prc c)
   | ConstrContext ((_,id),c) ->
       hov 0
-	(str "inst " ++ pr_id id ++ spc () ++
+	(str "context " ++ pr_id id ++ spc () ++
 	 str "[" ++ prlc c ++ str "]")
-  | ConstrTypeOf c -> hov 1 (str "check" ++ spc() ++ prc c)
-  | ConstrTerm c -> prlc c
+  | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c)
+  | ConstrTerm c -> prc c
 
 let pr_rawconstr_env_no_translate env c =
   pr lsimple (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 565da88caf..7b9ba49d8b 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -265,7 +265,7 @@ let pr_match_rule m pr pr_pat = function
   | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
 let pr_funvar = function
-  | None -> spc () ++ str "()"
+  | None -> spc () ++ str "_"
   | Some id -> spc () ++ pr_id id
 
 let pr_let_clause k pr = function
@@ -305,15 +305,15 @@ let pr_hintbases = function
 let pr_autoarg_adding = function
   | [] -> mt ()
   | l ->
-      spc () ++ str "Adding [" ++
+      spc () ++ str "adding [" ++
         hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
 
 let pr_autoarg_destructing = function
-  | true -> spc () ++ str "Destructing"
+  | true -> spc () ++ str "destructing"
   | false -> mt ()
 
 let pr_autoarg_usingTDB = function
-  | true -> spc () ++ str "Using TDB"
+  | true -> spc () ++ str "using tdb"
   | false -> mt ()
 
 let rec pr_tacarg_using_rule pr_gen = function
@@ -555,17 +555,16 @@ and pr_atom1 env = function
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) r ++
              pr_clause pr_ident h)
-  | TacChange (occ,c,h) -> (* A Verifier *)
+  | TacChange (occ,c,h) ->
       hov 1 (str "change" ++ brk (1,1) ++
       (match occ with
           None -> mt()
+        | Some([],c1) ->
+            hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
         | Some(ocl,c1) ->
             hov 1 (pr_constr env c1 ++ spc() ++
-	    if ocl <> [] then
-	      str "at " ++ prlist (fun i -> int i ++ spc()) ocl
-	    else
-	      mt ()) ++
-	    spc() ++ str "with ") ++
+	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "with ") ++
       pr_constr env c ++ pr_clause pr_ident h)
 
   (* Equivalence relations *)
@@ -632,7 +631,7 @@ let rec pr_tac env inherited tac =
       lmatch
   | TacMatchContext (lr,lrul) ->
       hov 0 (
-	str (if lr then "match reverse context with" else "match context with")
+	str (if lr then "match reverse goal with" else "match goal with")
 	++ prlist
 	  (fun r -> fnl () ++ str "| " ++
             pr_match_rule false (pr_tac env ltop) pr_pat r)
@@ -683,9 +682,11 @@ let rec pr_tac env inherited tac =
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
-  | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom
+  | TacArg(ConstrMayEval (ConstrTerm c)) ->
+      str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,l)) ->
       pr_with_comments loc
@@ -704,10 +705,11 @@ and pr_tacarg env = function
   | Identifier id -> pr_id id
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
-  | ConstrMayEval (ConstrTerm c) -> pr_constr env c
+  | ConstrMayEval c ->
+      pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
   | TacFreshId sopt -> str "fresh" ++ pr_opt qsnew sopt
-  | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
-      str "'" ++ pr_tac env (latom,E) (TacArg a)
+  | (TacCall _|Tacexp _|Integer _) as a ->
+      str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
 
 in ((fun env -> pr_tac env ltop),
     (fun env -> pr_tac env (latom,E)),
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index e2a4d22e42..2a8cc3c9b9 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -370,9 +370,9 @@ let pr_thm_token = function
   | Remark -> str"Remark"
 
 let pr_require_token = function
-  | Some true -> str "Export"
-  | Some false -> str "Import"
-  | None -> str "Closed"
+  | Some true -> str " Export"
+  | Some false -> str " Import"
+  | None -> mt()
 
 let pr_syntax_modifier = function
   | SetItemLevel (l,NextLevel) ->
@@ -718,7 +718,7 @@ let rec pr_vernac = function
           str key ++ spc() ++
           pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
 	  spc() ++ pr_type s ++ 
-	  str" :=") ++ pr_constructor_list lc ++ fnl () ++ 
+	  str" :=") ++ pr_constructor_list lc ++ 
 	pr_decl_notation pr_constr ntn in
 
       (* Copie simplifiée de command.ml pour déclarer les notations locales *)
@@ -833,7 +833,7 @@ let rec pr_vernac = function
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id)
   | VernacRequire (exp,spe,l) -> hov 2
-      (str "Require " ++ pr_require_token exp ++ spc() ++
+      (str "Require" ++ pr_require_token exp ++ spc() ++
       (match spe with
       |	None -> mt()
       |	Some flag ->