Imported Upstream version 8.1~gammaupstream/8.1.gamma

27 files changed, 786 insertions, 162 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 638a8d65..12c0ea1d 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: argextend.ml4 8976 2006-06-23 10:03:54Z herbelin $ *)
+(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
 
 open Genarg
 open Q_util
@@ -213,7 +213,7 @@ EXTEND
       [ e = argtype; LIDENT "list" -> List0ArgType e
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
-      [ e = LIDENT -> fst (interp_entry_name loc e) 
+      [ e = LIDENT -> fst (interp_entry_name loc e "")
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -221,7 +221,9 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name loc e in (g, Some (s,t))
+        let t, g = interp_entry_name loc e "" in (g, Some (s,t))
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = interp_entry_name loc e sep in (g, Some (s,t))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
 	    Pcoq.lexer.Token.using ("", s);
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 9ec7c532..07a0a65f 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: egrammar.ml 9333 2006-11-02 13:59:14Z barras $ *)
 
 open Pp
 open Util
@@ -196,23 +196,24 @@ let find_index s t =
   if s <> t or n = None then raise Not_found;
   out_some n
 
-let rec interp_entry_name up_level u s =
+let rec interp_entry_name up_level s =
   let l = String.length s in
   if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level u (String.sub s 3 (l-8)) in
+    let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in
     List1ArgType t, Gramext.Slist1 g
   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level u (String.sub s 0 (l-5)) in
+    let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in
     List0ArgType t, Gramext.Slist0 g
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name up_level u (String.sub s 0 (l-4)) in
+    let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in
     OptArgType t, Gramext.Sopt g
   else
+    let s = if s = "hyp" then "var" else s in
     try 
       let i = find_index "tactic" s in
       ExtraArgType s, 
-      if i=up_level then Gramext.Sself else
-      if i=up_level-1 then Gramext.Snext else
+      if up_level<>5 && i=up_level then Gramext.Sself else
+      if up_level<>5 && i=up_level-1 then Gramext.Snext else
       Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
     with Not_found ->
     let e = 
@@ -228,16 +229,18 @@ let rec interp_entry_name up_level u s =
     let t = type_of_typed_entry e in
     t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
 
-let make_vprod_item n univ = function
+let make_vprod_item n = function
   | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
   | VNonTerm (loc, nt, po) ->
-      let (etyp, e) = interp_entry_name n univ nt in
+      let (etyp, e) = interp_entry_name n nt in
       e, option_map (fun p -> (p,etyp)) po
 
 let get_tactic_entry n =
   if n = 0 then
     weaken_entry Tactic.simple_tactic, None
-  else if 1<=n && n<=5 then
+  else if n = 5 then
+    weaken_entry Tactic.binder_tactic, None
+  else if 1<=n && n<5 then
     weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
   else 
     error ("Invalid Tactic Notation level: "^(string_of_int n))
@@ -249,7 +252,7 @@ let head_is_ident = function VTerm _::_ -> true | _ -> false
 let add_tactic_entry (key,lev,prods,tac) =
   let univ = get_univ "tactic" in
   let entry, pos = get_tactic_entry lev in
-  let mkprod = make_vprod_item lev "tactic" in
+  let mkprod = make_vprod_item lev in
   let rules = 
     if lev = 0 then begin
       if not (head_is_ident prods) then
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 31247044..5dda69ba 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: egrammar.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -61,8 +61,7 @@ val get_extend_vernac_grammars :
 (*
 val reset_extend_grammars_v8 : unit -> unit
 *)
-val interp_entry_name : int -> string -> string -> 
-  entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a1c0c9ae..130c6804 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_constr.ml4 9043 2006-07-12 10:06:40Z herbelin $ *)
+(* $Id: g_constr.ml4 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 open Pcoq
 open Constr
@@ -155,8 +155,14 @@ GEXTEND Gram
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
-      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2)
-      | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ]
+      [ c1 = operconstr; "<:"; c2 = binder_constr -> 
+                 CCast(loc,c1, CastConv VMcast,c2)
+      | c1 = operconstr; "<:"; c2 = SELF -> 
+                 CCast(loc,c1, CastConv VMcast,c2)
+      | c1 = operconstr; ":";c2 = binder_constr -> 
+                 CCast(loc,c1, CastConv DEFAULTcast,c2)
+      | c1 = operconstr; ":"; c2 = SELF -> 
+                 CCast(loc,c1, CastConv DEFAULTcast,c2) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -287,7 +293,7 @@ GEXTEND Gram
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc 
-              (cases_pattern_loc p, "compound_pattern",
+              (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected"))
       | p = pattern; "as"; id = ident ->
 	  CPatAlias (loc, p, id) ]
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
new file mode 100644
index 00000000..8d7fd1f1
--- /dev/null
+++ b/parsing/g_decl_mode.ml4
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Decl_expr
+open Names
+open Term
+open Genarg
+open Pcoq
+
+open Pcoq.Constr
+open Pcoq.Tactic
+open Pcoq.Vernac_
+
+let none_is_empty = function
+    None -> []
+  | Some l -> l
+
+GEXTEND Gram
+GLOBAL: proof_instr;
+  thesis :
+    [[ "thesis" -> Plain 
+     | "thesis"; "for"; i=ident -> (For i)
+     | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n))
+     ]];
+  statement :
+    [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
+     | i=ident -> {st_label=Anonymous;
+		   st_it=Topconstr.CRef (Libnames.Ident (loc, i))}
+     | c=constr -> {st_label=Anonymous;st_it=c}
+     ]];
+  constr_or_thesis :
+     [[ t=thesis -> Thesis t ] |
+      [ c=constr -> This c
+      ]];
+  statement_or_thesis : 
+    [
+      [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] 
+    |
+      [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
+      | i=ident -> {st_label=Anonymous;
+		    st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))}
+      | c=constr -> {st_label=Anonymous;st_it=This c}
+      ]
+    ];
+  justification : 
+    [[ -> Automated [] 
+     | IDENT "by"; l=LIST1 constr SEP "," -> Automated l
+     | IDENT "by"; IDENT "tactic"; tac=tactic -> By_tactic tac ]]
+  ;
+  simple_cut_or_thesis :
+    [[ ls = statement_or_thesis;
+       j=justification -> {cut_stat=ls;cut_by=j} ]]
+  ;
+  simple_cut :
+    [[ ls = statement;
+       j=justification -> {cut_stat=ls;cut_by=j} ]]
+  ;
+  elim_type:
+    [[ IDENT "induction" -> ET_Induction
+     | IDENT "cases" -> ET_Case_analysis ]]
+  ;
+  block_type :
+    [[ IDENT "claim" -> B_claim
+     | IDENT "focus" -> B_focus
+     | IDENT "proof" -> B_proof
+     | et=elim_type -> B_elim et ]]
+  ;    
+  elim_obj:
+    [[ IDENT "on"; c=constr -> Real c
+     | IDENT "of"; c=simple_cut -> Virtual c ]]
+  ;    
+  elim_step:
+    [[ IDENT "consider" ; h=vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
+     | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)]]
+  ;
+  rew_step :
+    [[ "~=" ;         c=simple_cut -> (Rhs,c)       
+     | "=~" ;         c=simple_cut -> (Lhs,c)]]
+  ;
+  cut_step:
+    [[ "then"; tt=elim_step -> Pthen tt
+     | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
+     | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) 
+     | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
+     | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
+     | tt=elim_step -> tt
+     | tt=rew_step -> let s,c=tt in Prew (s,c); 
+     | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
+     | IDENT "claim"; c=statement -> Pclaim c;
+     | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;    
+     | "end"; bt = block_type -> Pend bt;
+     | IDENT "escape" -> Pescape ]]
+  ;
+  (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
+  loc_id: 
+    [[ id=ident -> fun x -> (loc,(id,x)) ]];
+  hyp:
+    [[ id=loc_id -> id None ;
+     | id=loc_id ; ":" ; c=constr -> id (Some c)]]
+  ;
+  vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=vars -> (Hvar name) :: v
+     | name=hyp; IDENT "be"; 
+       IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h
+     ]]
+  ;
+  hyps:  
+    [[ IDENT "we"; IDENT "have"; v=vars -> v
+     | st=statement; IDENT "and"; h=hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; v=vars  -> Hprop st::v
+     | st=statement -> [Hprop st]
+     ]]
+  ;
+  vars_or_thesis:
+    [[name=hyp -> [Hvar name] 
+     |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v
+     |name=hyp; OPT[IDENT "be"]; 
+      IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (Hvar name)::h
+     ]]
+  ;
+  hyps_or_thesis:  
+    [[ IDENT "we"; IDENT "have"; v=vars_or_thesis -> v
+     | st=statement_or_thesis; IDENT "and"; h=hyps_or_thesis  -> Hprop st::h
+     | st=statement_or_thesis; IDENT "and"; v=vars_or_thesis  -> Hprop st::v
+     | st=statement_or_thesis -> [Hprop st];
+     ]]
+  ;
+  intro_step:
+    [[ IDENT "suppose" ; h=hyps -> Psuppose h
+     | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
+       po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; 
+       ho=OPT[ IDENT "and" ; h=hyps_or_thesis -> h ] -> 
+	 Pcase (none_is_empty po,c,none_is_empty ho)
+     | "let" ; v=vars -> Plet v	 
+     | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
+     | IDENT "assume"; h=hyps -> Passume h
+     | IDENT "given"; h=vars -> Pgiven h
+     | IDENT "define"; id=ident; args=LIST0 hyp; 
+       "as"; body=constr -> Pdefine(id,args,body)
+     | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
+     | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
+     ]]
+  ;
+  emphasis : 
+    [[ -> 0
+     | "*" -> 1
+     | "**" -> 2
+     | "***" -> 3
+     ]]
+  ;
+  bare_proof_instr:
+    [[ c = cut_step -> c ;
+     | i = intro_step -> i ]]
+  ;
+  proof_instr :
+    [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]]
+  ;
+END;;
+
+ 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c01c23b6..27ff8140 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *)
+(* $Id: g_ltac.ml4 9333 2006-11-02 13:59:14Z barras $ *)
 
 open Pp
 open Util
@@ -43,38 +43,34 @@ let tacarg_of_expr = function
 (* Tactics grammar rules *)
 
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
+  GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
+          constr_may_eval;
 
   tactic_expr:
-    [ "5" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
+    [ "5" RIGHTA
+      [ te = binder_tactic -> te ]
+    | "4" LEFTA
+      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
+      | 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 ->
           TacAbstract (tc,Some s) ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
+      [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
+      | 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" ->
@@ -104,6 +100,17 @@ GEXTEND Gram
       [ "("; a = tactic_expr; ")" -> a
       | a = tactic_atom -> TacArg a ] ]
   ;
+  (* binder_tactic: level 5 of tactic_expr *)
+  binder_tactic:
+    [ RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+          TacFun (it,body)
+      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+          body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body)
+      | "let"; llc = LIST1 let_clause SEP "with"; "in";
+          u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u)
+      | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
+  ;
   (* Tactic arguments *)
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a
@@ -115,7 +122,10 @@ GEXTEND Gram
   ;
   may_eval_arg:
     [ [ c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ]
+      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ]
+  ;
+  fresh_id:
+    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 94205fa8..2f515a81 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_proofs.ml4 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: g_proofs.ml4 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Pcoq
 open Pp
@@ -75,6 +75,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
       | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+      | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
 	  VernacShow (ExplainProof l)
       | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a72ced97..9bbdc1d4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_vernac.ml4 9017 2006-07-05 17:27:34Z herbelin $ *)
+(* $Id: g_vernac.ml4 9306 2006-10-28 18:28:19Z herbelin $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -15,6 +15,7 @@ open Names
 open Topconstr
 open Vernacexpr
 open Pcoq
+open Decl_mode
 open Tactic
 open Decl_kinds
 open Genarg
@@ -34,13 +35,28 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 (* compilation on PowerPC and Sun architectures *)
 
 let check_command = Gram.Entry.create "vernac:check_command"
+
+let tactic_mode = Gram.Entry.create "vernac:tactic_command"
+let proof_mode = Gram.Entry.create "vernac:proof_command"
+let noedit_mode = Gram.Entry.create "vernac:noedit_command"
+
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
 
+let get_command_entry () =
+  match Decl_mode.get_current_mode () with
+      Mode_proof -> proof_mode
+    | Mode_tactic -> tactic_mode
+    | Mode_none -> noedit_mode
+
+let default_command_entry =
+  Gram.Entry.of_parser "command_entry" 
+    (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm)
+
 let no_hook _ _ = ()
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext;
+  GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
   vernac:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
@@ -54,9 +70,15 @@ GEXTEND Gram
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
   ;
-  vernac: LAST
-    [ [ gln = OPT[n=natural; ":" -> n];
-        tac = subgoal_command -> tac gln ] ]
+  vernac: LAST  
+    [ [ prfcom = default_command_entry -> prfcom ] ]
+  ;
+  noedit_mode:
+    [ [ c = subgoal_command -> c None] ]
+  ;
+  tactic_mode:
+  [ [ gln = OPT[n=natural; ":" -> n];
+      tac = subgoal_command -> tac gln ] ]
   ;
   subgoal_command:
     [ [ c = check_command; "." -> c
@@ -66,6 +88,12 @@ GEXTEND Gram
             let g = match g with Some gl -> gl | _ -> 1 in
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
+  proof_mode:
+    [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] 
+  ;
+  proof_mode: LAST
+    [ [ c=subgoal_command -> c (Some 1) ] ]
+  ; 
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
   ;
@@ -191,9 +219,9 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; 
+    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr;
         ":="; lc = constructor_list; ntn = decl_notation ->
-	  (id,ntn,indpar,c,lc) ] ]
+	  ((id,indpar,c,lc),ntn) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor SEP "|" -> l
@@ -212,7 +240,7 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = ident; bl = LIST1 binder_let;
-        annot = rec_annotation; type_ = type_cstr; 
+        annot = rec_annotation; ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
@@ -227,12 +255,12 @@ GEXTEND Gram
 		     otherwise, we search the recursive index later *)
 		  if List.length names = 1 then Some 0 else None	  
 	  in 
-	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
+	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
-        def = lconstr ->
-          (id,bl,c ,def) ] ]
+    [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":=";
+        def = lconstr; ntn = decl_notation ->
+          ((id,bl,ty,def),ntn) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
@@ -460,9 +488,8 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
 	  VernacDeclareMLModule l
 
-      (* Dump of the universe graph - to file or to stdout *) 
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
-	  VernacPrint (PrintUniverses fopt)
+	  error "This command is deprecated, use Print Universes"
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
@@ -556,7 +583,9 @@ GEXTEND Gram
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
         -> VernacRemoveOption (SecondaryTable (table,field), v)
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
-	  VernacRemoveOption (PrimaryTable table, v) ] ]
+	  VernacRemoveOption (PrimaryTable table, v) 
+      | IDENT "proof" -> VernacDeclProof
+      | "return" -> VernacReturn ]]
   ;
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
@@ -596,7 +625,8 @@ GEXTEND Gram
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid
+      | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index a89fffa0..c13532cc 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_xml.ml4 9016 2006-07-05 17:19:39Z herbelin $ *)
+(* $Id: g_xml.ml4 9200 2006-10-03 14:11:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -146,9 +146,11 @@ let rec interp_xml_constr = function
       let ctx = List.map interp_xml_decl decls in
       List.fold_right (fun (na,t) b -> RProd (loc, na, t, b))
 	ctx (interp_xml_target body)
-  | XmlTag (loc,"LETIN",al,[x1;x2]) ->
-      let na,t = interp_xml_def x1 in
-      RLetIn (loc, na, t, interp_xml_target x2) 
+  | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
+      let body,defs = list_sep_last xl in
+      let ctx = List.map interp_xml_def defs in
+      List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b))
+        ctx (interp_xml_target body)
   | XmlTag (loc,"APPLY",_,x::xl) ->
       RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
   | XmlTag (loc,"instantiate",_,
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 56e434fb..f7adfdd8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.ml4 9043 2006-07-12 10:06:40Z herbelin $ i*)
+(*i $Id: pcoq.ml4 9333 2006-11-02 13:59:14Z barras $ i*)
 
 open Pp
 open Util
@@ -430,6 +430,7 @@ module Tactic =
     (* Main entries for ltac *)
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
     let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
+    let binder_tactic = Gram.Entry.create "tactic:binder_tactic"
 
     let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
@@ -451,6 +452,12 @@ module Vernac_ =
     let syntax = gec_vernac "syntax_command"
     let vernac = gec_vernac "Vernac_.vernac"
 
+    (* MMode *)
+
+    let proof_instr = Gram.Entry.create "proofmode:instr"
+
+    (* /MMode *)
+
     let vernac_eoi = eoi_entry vernac
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3998d71b..1fe8c122 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.mli 8926 2006-06-08 20:23:17Z herbelin $ i*)
+(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*)
 
 open Util
 open Names
@@ -184,6 +184,7 @@ module Tactic :
     val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
     val tactic_arg : raw_tactic_arg Gram.Entry.e
     val tactic_expr : raw_tactic_expr Gram.Entry.e
+    val binder_tactic : raw_tactic_expr Gram.Entry.e
     val tactic : raw_tactic_expr Gram.Entry.e
     val tactic_eoi : raw_tactic_expr Gram.Entry.e
   end
@@ -196,6 +197,13 @@ module Vernac_ :
     val command : vernac_expr Gram.Entry.e
     val syntax : vernac_expr Gram.Entry.e
     val vernac : vernac_expr Gram.Entry.e
+    
+  (* MMode *)
+
+    val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e
+
+  (*/ MMode *)
+
     val vernac_eoi : vernac_expr Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a1ca386e..349d5df8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml 8997 2006-07-03 16:40:20Z herbelin $ *)      
+(* $Id: ppconstr.ml 9304 2006-10-28 09:58:16Z herbelin $ *)      
 
 (*i*)
 open Util
@@ -95,8 +95,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let surround p = hov 1 (str"(" ++ p ++ str")")
-
 let pr_located pr ((b,e),x) =
   if Options.do_translate() && (b,e)<>dummy_loc then
     let (b,e) = unloc (b,e) in
@@ -115,12 +113,14 @@ let pr_optc pr = function
   | None -> mt ()
   | Some x -> pr_sep_com spc pr x
 
+let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+
 let pr_universe = Univ.pr_uni 
 
 let pr_rawsort = function
   | RProp Term.Null -> str "Prop"
   | RProp Term.Pos -> str "Set"
-  | RType u -> str "Type" ++ pr_opt pr_universe u
+  | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
 
 let pr_id = pr_id
 let pr_name = pr_name
@@ -180,7 +180,7 @@ let rec pr_patt sep inh p =
   | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
-  let loc = cases_pattern_loc p in
+  let loc = cases_pattern_expr_loc p in
   pr_with_comments loc
     (sep() ++ if prec_less prec inh then strm else surround strm)
 
@@ -566,8 +566,9 @@ let rec pr sep inherited a =
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_rawsort s, latom
-  | CCast (_,a,_,b) ->
-      hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
+  | CCast (_,a,k,b) ->
+      let s = match k with CastConv  VMcast -> "<:" | _ -> ":" in
+      hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
       lcast
   | CNotation (_,"( _ )",[t]) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
new file mode 100644
index 00000000..7e57885c
--- /dev/null
+++ b/parsing/ppdecl_proof.ml
@@ -0,0 +1,180 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util 
+open Pp
+open Decl_expr
+open Names 
+open Nameops
+
+let pr_constr = Printer.pr_constr_env
+let pr_tac = Pptactic.pr_glob_tactic
+let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr 
+
+let pr_label = function
+    Anonymous -> mt ()
+  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () 
+
+let pr_justification env = function
+    Automated [] -> mt ()
+  | Automated (_::_ as l) -> 
+      spc () ++ str "by" ++ spc () ++  
+	prlist_with_sep (fun () -> str ",") (pr_constr env) l
+  | By_tactic tac -> 
+      spc () ++ str "by" ++ spc () ++ str "tactic" ++  pr_tac env tac
+
+let pr_statement pr_it env st = 
+  pr_label st.st_label ++ pr_it env st.st_it
+
+let pr_or_thesis pr_this env = function
+    Thesis Plain -> str "thesis"
+  | Thesis (For id) -> 
+      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id 
+  | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]"
+  | This c -> pr_this env c
+
+let pr_cut pr_it env c = 
+  hov 1 (pr_statement pr_it env c.cut_stat) ++ 
+    pr_justification env c.cut_by
+
+let type_or_thesis = function
+    Thesis _ -> Term.mkProp
+  | This c -> c
+
+let _I x = x
+
+let rec print_hyps pconstr gtyp env _and _be hyps = 
+  let _andp = if _and then str "and" ++spc () else mt () in
+    match hyps with 
+	(Hvar _ ::_) as rest -> 
+	  spc () ++ _andp ++ str "we have" ++ 
+	    print_vars pconstr gtyp env false _be rest
+      | Hprop st :: rest -> 
+	  begin
+	    let nenv =
+	      match st.st_label with
+		  Anonymous -> env
+		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
+	      spc() ++ _andp ++ pr_statement pconstr env st ++ 
+		print_hyps pconstr gtyp nenv true _be rest
+	  end
+      | [] -> mt ()
+
+and print_vars pconstr gtyp env _and _be vars =
+  match vars with
+    Hvar st :: rest -> 
+      begin
+	let nenv = 
+	  match st.st_label with
+	      Anonymous -> anomaly "anonymous variable"
+	    | Name id -> Environ.push_named (id,None,st.st_it) env in
+	let _andp = if _and then pr_coma () else mt () in
+		spc() ++ _andp ++
+		   pr_statement pr_constr env st ++
+		  print_vars pconstr gtyp nenv true _be rest
+      end
+   | (Hprop _ :: _) as rest ->
+      let _st =  if _be then 
+	str "be such that" 
+      else 
+	str "such that" in
+	spc() ++ _st ++  print_hyps pconstr gtyp env false _be rest
+  | [] -> mt ()
+
+let pr_elim_type = function
+    ET_Case_analysis -> str "cases"
+  | ET_Induction -> str "induction"
+
+let pr_casee env =function
+    Real c -> str "on" ++ spc () ++ pr_constr env c
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr env cut
+
+let pr_side = function
+    Lhs -> str "=~"
+  | Rhs -> str "~="
+
+let rec pr_bare_proof_instr _then _thus env = function
+  | Pescape -> str "escape"
+  | Pthen i -> pr_bare_proof_instr true _thus env i 
+  | Pthus i -> pr_bare_proof_instr _then true env i 
+  | Phence i -> pr_bare_proof_instr true true env i
+  | Pcut c -> 
+      begin
+	match _then,_thus with
+	    false,false -> str "have" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | false,true  -> str "thus" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | true,false  -> str "then" ++ spc () ++
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | true,true   -> str "hence" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+      end
+  | Prew (sid,c) ->
+      (if _thus then str "thus" else str "    ") ++ spc () ++
+	pr_side sid ++ spc () ++ pr_cut pr_constr env c
+  | Passume hyps -> 
+      str "assume" ++ print_hyps pr_constr _I env false false hyps
+  | Plet hyps -> 
+      str "let" ++ print_vars pr_constr _I env false true hyps
+  | Pclaim st ->
+      str "claim" ++ spc () ++ pr_statement pr_constr env st
+  | Pfocus st ->
+      str "focus on" ++ spc () ++ pr_statement pr_constr env st
+  | Pconsider (id,hyps) ->
+      str "consider" ++ print_vars pr_constr _I env false false hyps 
+      ++ spc () ++ str "from " ++ pr_constr env id 
+  | Pgiven hyps ->
+      str "given" ++ print_vars pr_constr _I env false false hyps
+  | Ptake witl -> 
+      str "take" ++ spc () ++ 
+	prlist_with_sep pr_coma (pr_constr env) witl
+  | Pdefine (id,args,body) ->
+      str "define" ++ spc () ++ pr_id id ++ spc () ++ 
+	prlist_with_sep spc 
+	(fun st -> str "(" ++ 
+	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++ 
+	str "as" ++ (pr_constr env body) 
+  | Pcast (id,typ) -> 
+      str "reconsider" ++ spc () ++ 
+	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ 
+	str "as" ++ (pr_constr env typ)  
+  | Psuppose hyps -> 
+      str "suppose" ++ 
+	print_hyps pr_constr _I env false false hyps
+  | Pcase (params,pat,hyps) ->
+      str "suppose it is" ++ spc () ++ pr_pat pat ++
+	(if params = [] then mt () else 
+	   (spc () ++ str "with" ++ spc () ++ 
+	      prlist_with_sep spc 
+	      (fun st -> str "(" ++ 
+		 pr_statement pr_constr env st ++ str ")") params ++ spc ())) 
+      ++
+	(if hyps = [] then mt () else 
+	   (spc () ++ str "and" ++ 
+	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
+	      env false false hyps))
+  | Pper (et,c) -> 
+      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
+      pr_casee env c
+  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
+  | _ -> anomaly "unprintable instruction"
+
+let pr_emph = function
+    0 -> str "    "
+  | 1 -> str "*   "
+  | 2 -> str "**  "
+  | 3 -> str "*** "
+  | _ -> anomaly "unknown emphasis"
+
+let pr_proof_instr env instr = 
+  pr_emph instr.emph ++ spc () ++ 
+    pr_bare_proof_instr false false env instr.instr
+
diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli
new file mode 100644
index 00000000..b0f0e110
--- /dev/null
+++ b/parsing/ppdecl_proof.mli
@@ -0,0 +1,2 @@
+
+val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds  
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2113ae89..c7e1db60 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *)
 
 open Pp
 open Names
@@ -127,6 +127,8 @@ let rec pr_message_token prid = function
   | MsgInt n -> int n
   | MsgIdent id -> prid id
 
+let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
+
 let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
@@ -261,8 +263,6 @@ let rec pr_tacarg_using_rule pr_gen = function
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let surround p = hov 1 (str"(" ++ p ++ str")")
-
 let pr_extend_gen prgen lev s l =
   try 
     let tags = List.map genarg_tag l in
@@ -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),
@@ -902,7 +903,7 @@ let rec pr_tac inherited tac =
       str "constr:" ++ pr_constr c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval pr_constr pr_lconstr pr_cst c, leval
-  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
+  | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,l)) ->
       pr_with_comments loc
@@ -923,7 +924,7 @@ and pr_tacarg = function
   | Reference r -> pr_ref r
   | ConstrMayEval c ->
       pr_may_eval pr_constr pr_lconstr pr_cst c
-  | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
+  | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacExternal (_,com,req,la) ->
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ 
       spc() ++ prlist_with_sep spc pr_tacarg la
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 7e3c853d..f86b5708 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 9020 2006-07-05 17:35:23Z herbelin $ *)  
+(* $Id: ppvernac.ml 9154 2006-09-20 17:18:18Z corbinea $ *)  
 
 open Pp
 open Names
@@ -410,6 +410,7 @@ let rec pr_vernac = function
 	| ShowProofNames -> str"Show Conjectures"
 	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
 	| ShowMatch id -> str"Show Match " ++ pr_lident id
+	| ShowThesis -> str "Show Thesis"
 	| ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l
 	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l 
       in pr_showable s
@@ -530,7 +531,7 @@ let rec pr_vernac = function
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
-      let pr_oneind key (id,ntn,indpar,s,lc) =
+      let pr_oneind key ((id,indpar,s,lc),ntn) =
 	hov 0 (
           str key ++ spc() ++
           pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
@@ -585,14 +586,16 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint (corecs,b) ->
-      let pr_onecorec (id,bl,c,def) =
+      let pr_onecorec ((id,bl,c,def),ntn) =
         let (bl',def,c) =
               if Options.do_translate() then extract_def_binders def c
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
-        str" :=" ++ brk(1,1) ++ pr_lconstr def in
+        str" :=" ++ brk(1,1) ++ pr_lconstr def  ++ 
+	pr_decl_notation pr_constr ntn
+      in
       let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
       hov 1 (str start ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
@@ -679,6 +682,14 @@ let rec pr_vernac = function
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c
 
+  (* MMode *)
+ 
+  | VernacProofInstr instr -> anomaly "Not implemented"
+  | VernacDeclProof -> str "proof" 
+  | VernacReturn -> str "return"
+
+  (* /MMode *) 
+
   (* Auxiliary file and library management *)
   | VernacRequireFrom (exp,spe,f) -> hov 2
       (str"Require" ++ spc() ++ pr_require_token exp ++
@@ -820,7 +831,7 @@ let rec pr_vernac = function
 
   (* For extension *)
   | VernacExtend (s,c) -> pr_extend s c
-  | VernacProof Tacexpr.TacId _ -> str "Proof"
+  | VernacProof (Tacexpr.TacId _) -> str "Proof"
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
 
 and pr_extend s cl =
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4534369f..57028469 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: prettyp.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -246,6 +246,7 @@ let print_safe_judgment env j =
 let print_named_def name body typ =
   let pbody = pr_lconstr body in
   let ptyp = pr_ltype typ in
+  let pbody = if isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
@@ -278,11 +279,15 @@ let print_constructors envpar names types =
   hv 0 (str "  " ++ pc)
 
 let build_inductive sp tyi =
-  let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in
+  let (mib,mip) = Global.lookup_inductive (sp,tyi) in
   let params = mib.mind_params_ctxt in
   let args = extended_rel_list 0 params in
   let env = Global.env() in
-  let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in
+  let fullarity = match mip.mind_arity with
+    | Monomorphic ar -> ar.mind_user_arity 
+    | Polymorphic ar ->
+	it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
+  let arity = hnf_prod_applist env fullarity args in
   let cstrtypes = arities_of_constructors env (sp,tyi) in
   let cstrtypes =
     Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -325,10 +330,14 @@ let print_body = function
 let print_typed_body (val_0,typ) =
   (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ ++ fnl ())
 
+let ungeneralized_type_of_constant_type = function
+  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+  | NonPolymorphicType t -> t
+
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = cb.const_body in
-  let typ = cb.const_type in
+  let typ = ungeneralized_type_of_constant_type cb.const_type in
   hov 0 (
     match val_0 with 
     | None -> 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 8cb5ac42..c0a98809 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
+(* $Id: printer.ml 9164 2006-09-23 09:36:05Z herbelin $ *)
 
 open Pp
 open Util
@@ -23,6 +23,7 @@ open Nametab
 open Ppconstr
 open Evd
 open Proof_type
+open Decl_mode
 open Refiner
 open Pfedit
 open Ppconstr
@@ -108,6 +109,13 @@ let pr_evaluable_reference ref =
   | EvalVarRef sp -> VarRef sp in
  pr_global ref'
 
+(*let pr_rawterm t =
+  pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
+
+(*open Pattern
+
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
+
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
@@ -117,6 +125,7 @@ let pr_var_decl env (id,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
 	(str" := " ++ pb ++ cut () ) in
   let pt = pr_ltype_env env typ in
   let ptyp = (str" : " ++ pt) in
@@ -128,6 +137,7 @@ let pr_rel_decl env (na,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = pr_lconstr_env env c in
+	let pb = if isCast c then surround pb else pb in
 	(str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = pr_ltype_env env typ in
   match na with
@@ -219,23 +229,53 @@ let pr_context_of env = match Options.print_hyps_limit () with
   | None -> hv 0 (pr_context_unlimited env)
   | Some n -> hv 0 (pr_context_limit n env)
 
+(* display goal parts (Proof mode) *)
+
+let pr_restricted_named_context among env =
+  hv 0 (fold_named_context
+	  (fun env ((id,_,_) as d) pps ->
+	     if true || Idset.mem id among then
+	       pps ++ 
+		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++
+		 pr_var_decl env d
+	     else 
+	       pps)
+          env ~init:(mt ()))
+
+let pr_subgoal_metas metas env=
+  let pr_one (meta,typ) = 
+    str "?" ++ int meta ++ str " : " ++ 
+      hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ 
+      str (emacs_str (String.make 1 (Char.chr 253))) in
+    hv 0 (prlist_with_sep mt pr_one metas)
 
 (* display complete goal *)
 let pr_goal g =
   let env = evar_env g in
-  let penv = pr_context_of env in
-  let pc = pr_ltype_env_at_top env g.evar_concl in
-  str"  " ++ hv 0 (penv ++ fnl () ++
-		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
-                   str "============================" ++ fnl ()  ++
-                   str" "  ++ pc) ++ fnl ()
-
+  let preamb,penv,pc =
+    if g.evar_extra = None then
+          mt (),
+	  pr_context_of env,
+	  pr_ltype_env_at_top env g.evar_concl
+    else 
+      let {pm_subgoals=metas;pm_hyps=among} = get_info g in
+	(str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
+    pr_restricted_named_context among env,
+    pr_subgoal_metas metas env
+  in
+    preamb ++
+    str"  " ++ hv 0 (penv ++ fnl () ++
+		       str (emacs_str (String.make 1 (Char.chr 253)))  ++
+		       str "============================" ++ fnl ()  ++
+		       str" "  ++ pc) ++ fnl ()
+     
 (* display the conclusion of a goal *)
 let pr_concl n g =
   let env = evar_env g in
   let pc = pr_ltype_env_at_top env g.evar_concl in
-  str (emacs_str (String.make 1 (Char.chr 253)))  ++
-  str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+    str (emacs_str (String.make 1 (Char.chr 253)))  ++
+      str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl = 
@@ -266,15 +306,22 @@ let pr_subgoal n =
   prrec n
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
-let pr_subgoals sigma = function 
+let pr_subgoals close_cmd sigma = function 
   | [] -> 
-      let exl = Evarutil.non_instantiated sigma in 
-      if exl = [] then 
-	(str"Proof completed."  ++ fnl ())
-      else
-        let pei = pr_evars_int 1 exl in
-        (str "No more subgoals but non-instantiated existential " ++
-           str "variables :"  ++fnl () ++ (hov 0 pei))
+      begin
+	match close_cmd with
+	  Some cmd ->
+	    (str "Subproof completed, now type " ++ str cmd ++ 
+	       str "." ++ fnl ())
+	| None ->
+	    let exl = Evarutil.non_instantiated sigma in 
+	      if exl = [] then 
+		(str"Proof completed."  ++ fnl ())
+	      else
+		let pei = pr_evars_int 1 exl in
+		  (str "No more subgoals but non-instantiated existential " ++
+		     str "variables :"  ++fnl () ++ (hov 0 pei))
+      end
   | [g] ->
       let pg = pr_goal g in
       v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
@@ -291,12 +338,12 @@ let pr_subgoals sigma = function
       v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
 	   ++ pg1 ++ prest ++ fnl ())
 
-
-let pr_subgoals_of_pfts pfts = 
+let pr_subgoals_of_pfts pfts =
+  let close_cmd = Decl_mode.get_end_command pfts in
   let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
   let sigma = (top_goal_of_pftreestate pfts).sigma in
-  pr_subgoals sigma gls
-
+    pr_subgoals close_cmd sigma gls
+      
 let pr_open_subgoals () =
   let pfts = get_pftreestate () in
   match focus() with
@@ -351,7 +398,6 @@ let pr_prim_rule = function
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
         | [] -> mt () in
       (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
-
   | Refine c -> 
       str(if occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 9d59bf75..6795889c 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: printer.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
+(*i $Id: printer.mli 9249 2006-10-19 07:46:03Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -35,6 +35,7 @@ val pr_lconstr             : constr -> std_ppcmds
 val pr_constr_env          : env -> constr -> std_ppcmds
 val pr_constr              : constr -> std_ppcmds
 
+val pr_ltype_env_at_top    : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds
 
@@ -87,7 +88,7 @@ val pr_context_of          : env -> std_ppcmds
 (* Proofs *)
 
 val pr_goal                : goal -> std_ppcmds
-val pr_subgoals            : evar_map -> goal list -> std_ppcmds
+val pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds
 val pr_subgoal             : int -> goal list -> std_ppcmds
 
 val pr_open_subgoals       : unit -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b5b07091..23d24497 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: q_coqast.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: q_coqast.ml4 9315 2006-10-29 21:53:30Z barras $ *)
 
 open Util
 open Names
@@ -441,8 +441,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
         $mlexpr_of_bool lz$
         $mlexpr_of_bool lr$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
+
+  | Tacexpr.TacFun (idol,body) ->
+      <:expr< Tacexpr.TacFun
+        ($mlexpr_of_list mlexpr_of_ident_option idol$,
+         $mlexpr_of_tactic body$) >>
 (*
-  | Tacexpr.TacFun of $dloc$ * tactic_fun_ast
   | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast
 *)
 (*
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 61a552f3..2ef56907 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: q_util.ml4 8982 2006-06-23 13:17:49Z herbelin $ *)
+(* $Id: q_util.ml4 9333 2006-11-02 13:59:14Z barras $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
@@ -71,22 +71,46 @@ open Vernacexpr
 open Pcoq
 open Genarg
 
-let rec interp_entry_name loc s =
+let modifiers e =
+<:expr<  Gramext.srules
+    [([], Gramext.action(fun _loc -> []));
+     ([Gramext.Stoken ("", "(");
+       Gramext.Slist1sep ($e$, Gramext.Stoken ("", ","));
+       Gramext.Stoken ("", ")")],
+      Gramext.action (fun _ l _ _loc -> l))]
+ >>
+
+let rec interp_entry_name loc s sep =
   let l = String.length s in
   if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) "" in
     List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+  else if l > 12 & String.sub s 0 3 = "ne_" &
+                   String.sub s (l-9) 9 = "_list_sep" then
+    let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in
+    let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in
+    List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >>
   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in
     List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+  else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in
+    let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in
+    List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >>
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
+  else if l > 5 & String.sub s (l-5) 5 = "_mods" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-1)) "" in
+    List0ArgType t, modifiers g
   else
     let s = if s = "hyp" then "var" else s in
     let t, se, lev =
       match tactic_genarg_level s with
-	| Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
+        | Some 5 ->
+            Some (ExtraArgType s), <:expr< Tactic. binder_tactic >>, None
+	| Some n ->
+            Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
 	| None ->
       match Pcoq.entry_type (Pcoq.get_univ "prim") s with
 	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index d31b217c..901f9198 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: q_util.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: q_util.mli 9265 2006-10-24 08:35:38Z herbelin $ i*)
 
 val patt_of_expr : MLast.expr -> MLast.patt
 
@@ -28,4 +28,5 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val interp_entry_name : Util.loc -> string -> Pcoq.entry_type * MLast.expr
+val interp_entry_name : Util.loc -> string -> string -> 
+  Pcoq.entry_type * MLast.expr
diff --git a/parsing/search.ml b/parsing/search.ml
index 995aa953..28362d72 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: search.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: search.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Pp
 open Util
@@ -57,12 +57,12 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	     fn (VarRef idc) env typ
 	 with Not_found -> (* we are in a section *) ())
     | "CONSTANT" ->
-	let kn = locate_constant (qualid_of_sp sp) in
-	let {const_type=typ} = Global.lookup_constant kn in
+	let cst = locate_constant (qualid_of_sp sp) in
+	let typ = Typeops.type_of_constant env cst in
         if refopt = None
 	  || head_const typ = constr_of_global (out_some refopt)
 	then
-	  fn (ConstRef kn) env typ
+	  fn (ConstRef cst) env typ
     | "INDUCTIVE" -> 
 	let kn = locate_mind (qualid_of_sp sp) in
         let mib = Global.lookup_mind kn in 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 3d41e388..73d41465 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
 
 open Genarg
 open Q_util
@@ -165,7 +165,7 @@ let declare_tactic loc s cl =
       open Pcoq;
       declare $list:hidden$ end;
       try
-        let _=Refiner.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
+        let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
         List.iter
           (fun s -> Tacinterp.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
@@ -198,7 +198,10 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = Q_util.interp_entry_name loc e in
+        let t, g = Q_util.interp_entry_name loc e "" in
+        TacNonTerm (loc, t, g, Some s)
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = Q_util.interp_entry_name loc e sep in
         TacNonTerm (loc, t, g, Some s)
       | s = STRING ->
 	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 3584e375..6ea1c97e 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactic_printer.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: tactic_printer.ml 9244 2006-10-16 17:11:44Z barras $ *)
 
 open Pp
 open Util
@@ -15,6 +15,7 @@ open Evd
 open Tacexpr
 open Proof_type
 open Proof_trees
+open Decl_expr
 open Logic
 open Printer
 
@@ -25,19 +26,34 @@ let pr_tactic = function
   | t -> 
       Pptactic.pr_tactic (Global.env()) t
 
+let pr_proof_instr instr = 
+    Ppdecl_proof.pr_proof_instr (Global.env()) instr
+
 let pr_rule = function
   | Prim r -> hov 0 (pr_prim_rule r)
-  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+  | Nested(cmpd,_) ->
+      begin
+	match cmpd with 
+	    Tactic (texp,_) -> hov 0 (pr_tactic texp)
+	  | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
+      end
+  | Daimon -> str "<Daimon>"
+  | Decl_proof _ -> str "proof" 
   | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level.
          Function pr_rule_dot below is used when we want to hide
          Change_evars *)
       str "Evar change"
 
+let uses_default_tac = function
+  | Nested(Tactic(_,dflt),_) -> dflt
+  | _ -> false
+
 (* Does not print change of evars *)
 let pr_rule_dot = function 
   | Change_evars -> mt ()
-  | r -> pr_rule r ++ str"."
+  | r ->
+      pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
 exception Different
 
@@ -52,59 +68,145 @@ let thin_sign osign sign =
     sign ~init:Environ.empty_named_context_val
 
 let rec print_proof sigma osign pf =
-  let {evar_hyps=hyps; evar_concl=cl; 
-       evar_body=body} = pf.goal in
-  let hyps = Environ.named_context_of_val hyps in
+  let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
-	hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
+	hov 0 (pr_goal {pf.goal with evar_hyps=hyps'})
     | Some(r,spfl) ->
     	hov 0 
-	  (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
+	  (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++
 	   spc () ++ str" BY " ++
 	   hov 0 (pr_rule r) ++ fnl () ++
 	   str"  " ++
-	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
-)
+	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
 	  
 let pr_change gl = 
-  str"Change " ++
+  str"change " ++
   pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
 
-let rec print_script nochange sigma osign pf =
-  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
-  let sign = Environ.named_context_of_val sign in
+let rec print_decl_script tac_printer nochange sigma pf =
+  match pf.ref with
+    | None ->
+	(if nochange then 
+	   (str"<Your Proof Text here>")
+	 else 
+	   pr_change pf.goal)
+	++ fnl ()
+    | Some (Daimon,_) -> mt ()
+    | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
+	begin
+	  match instr.instr,subprfs with
+	    Pescape,[{ref=Some(_,subsubprfs)}] ->
+	      hov 7
+		(pr_rule_dot rule ++ fnl () ++
+		   prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
+		if opened then mt () else str "return."
+	  | Pclaim _,[body;cont] ->
+	      hov 2
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		if opened then mt () else str "end claim." ++ fnl () ++
+		  print_decl_script tac_printer nochange sigma cont
+	  | Pfocus _,[body;cont] ->
+	      hov 2 
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		if opened then mt () else str "end focus." ++ fnl () ++
+		  print_decl_script tac_printer nochange sigma cont
+	  | (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
+	      hov 2 
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		print_decl_script tac_printer nochange sigma cont 
+	  | _,[next] ->
+	      pr_rule_dot rule ++ fnl () ++
+		print_decl_script tac_printer nochange sigma next
+	  | _,[] ->
+	      pr_rule_dot rule		
+	  | _,_ -> anomaly "unknown branching instruction"
+	end
+    | _ -> anomaly "Not Applicable"
+
+let rec print_script nochange sigma pf =
   match pf.ref with
     | None ->
         (if nochange then 
-	  (str"<Your Tactic Text here>") 
-	else 
-	  pr_change pf.goal)
+	   (str"<Your Tactic Text here>") 
+	 else 
+	   pr_change pf.goal)
 	++ fnl ()
-    | Some(r,spfl) ->
-        ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-           pr_rule_dot r ++ fnl () ++
-           prlist_with_sep pr_fnl
-             (print_script nochange sigma sign) spfl)
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) 
+	end ++
+	  begin
+	    hov 0 (str "proof." ++ fnl () ++ 
+		     print_decl_script (print_script nochange sigma) 
+		     nochange sigma (List.hd script))
+	  end ++ fnl () ++
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )
+    | Some(rule,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   pr_rule_dot rule ++ fnl () ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )	
 
 (* printed by Show Script command *)
-let print_treescript nochange sigma _osign pf =
+
+let print_treescript nochange sigma pf =
   let rec aux top pf =
     match pf.ref with
     | None ->
         if nochange then 
-	  (str"<Your Tactic Text here>") 
+	  if pf.goal.evar_extra=None then
+	    (str"<Your Tactic Text here>")
+	  else (str"<Your Proof Text here>")
 	else 
 	  (pr_change pf.goal)
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
+	end ++
+	  hov 0 
+	  begin str "proof." ++ fnl () ++
+	    print_decl_script (aux false)  
+	    nochange sigma (List.hd script) 
+	  end ++ fnl () ++ 
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )
     | Some(r,spfl) ->
         (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
-	pr_rule_dot r ++
-	match spfl with
-	| [] -> mt ()
-	| [spf] -> fnl () ++ (if top then mt () else str "  ") ++ aux top spf
-	| _ -> fnl () ++ str " " ++
-	    hov 0 (prlist_with_sep fnl (aux false) spfl)
+	  pr_rule_dot r ++
+	  begin
+	    if List.length spfl > 1 then
+	      fnl ()  ++ 
+		str " " ++  hov 0 (aux false (List.hd spfl)) ++ fnl () ++
+		hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl))
+	    else
+	      match spfl with
+		| [] -> mt ()
+		| [spf] -> fnl () ++ 
+		    (if top then mt () else str "  ") ++ aux top spf
+		| _ -> fnl () ++ str " " ++
+		    hov 0 (prlist_with_sep fnl (aux false) spfl)
+	  end
   in hov 0 (aux true pf)
 
 let rec print_info_script sigma osign pf =
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index db5dd794..b1f6d41c 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactic_printer.mli 6113 2004-09-17 20:28:19Z barras $ i*)
+(*i $Id: tactic_printer.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Pp
@@ -22,6 +22,6 @@ val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
 val pr_rule     : rule -> std_ppcmds
 val pr_tactic   : tactic_expr -> std_ppcmds
 val print_script :
-  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+  bool -> evar_map -> proof_tree -> std_ppcmds
 val print_treescript :
-  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+  bool -> evar_map -> proof_tree -> std_ppcmds
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index af0d6781..7cf542fe 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernacextend.ml4 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
 
 open Genarg
 open Q_util
@@ -114,7 +114,7 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = Q_util.interp_entry_name loc e in
+        let t, g = Q_util.interp_entry_name loc e "" in
         VernacNonTerm (loc, t, g, Some s)
       | s = STRING ->
         VernacTerm s