fixed field_simplify + changed precedence of let and fun in ltac

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

2 files changed, 16 insertions, 15 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2e72784b5..cd447e537 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -46,20 +46,26 @@ GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
 
   tactic_expr:
-    [ "5" LEFTA
+    [ "5" RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
+          TacFun (it,body)
+      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+          body = tactic_expr -> TacLetRecIn (rcl,body)
+      | "let"; llc = LIST1 let_clause SEP "with"; "in";
+          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
+      | IDENT "info"; tc = tactic_expr -> TacInfo tc ]
+      
+    | "4" LEFTA
       [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
 	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
 	  TacThens (ta, lta) ]
-    | "4"
-      [ ]
     | "3" RIGHTA
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
-      | IDENT "info"; tc = tactic_expr -> TacInfo tc
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
@@ -68,13 +74,7 @@ GEXTEND Gram
     | "2" RIGHTA
       [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
-          TacFun (it,body)
-      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
-          body = tactic_expr -> TacLetRecIn (rcl,body)
-      | "let"; llc = LIST1 let_clause SEP "with"; "in";
-          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-      | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
+      [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (b,false,mrl)
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fdb0ff503..451313be5 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -521,11 +521,11 @@ let rec pr_tacarg_using_rule pr_gen = function
 let pr_then () = str ";"
 
 let ltop = (5,E)
-let lseq = 5
+let lseq = 4
 let ltactical = 3
 let lorelse = 2
-let llet = 1
-let lfun = 1
+let llet = 5
+let lfun = 5
 let lcomplete = 1
 let labstract = 3
 let lmatch = 1
@@ -533,6 +533,7 @@ let latom = 0
 let lcall = 1
 let leval = 1
 let ltatom = 1
+let linfo = 5
 
 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
@@ -875,7 +876,7 @@ let rec pr_tac inherited tac =
       ltactical
   | TacInfo t ->
       hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
+      linfo
   | TacOrelse (t1,t2) ->
       hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),