Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

13 files changed, 210 insertions, 138 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 130c6804..9163f3c1 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 9226 2006-10-09 16:11:01Z herbelin $ *)
+(* $Id: g_constr.ml4 9562 2007-01-31 09:00:36Z msozeau $ *)
 
 open Pcoq
 open Constr
@@ -249,8 +249,8 @@ GEXTEND Gram
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
-      | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
-      | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel)
+      | "{"; IDENT "wf"; rel=constr; id=name; "}" -> (Some id, CWfRec rel)
+      | "{"; IDENT "measure"; rel=constr; id=name; "}" -> (Some id, CMeasureRec rel)
       | ->  (None, CStructRec)
       ] ]
   ;
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 8d7fd1f1..5c7b40af 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Decl_expr
@@ -50,18 +50,26 @@ GLOBAL: proof_instr;
       | 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 ]]
+  justification_items : 
+    [[ -> Some [] 
+     | IDENT "by"; l=LIST1 constr SEP "," -> Some l
+     | IDENT "by"; "*"                    -> None ]]
+  ;
+  justification_method : 
+    [[ -> None 
+     | "using";  tac = tactic -> Some tac ]]
   ;
   simple_cut_or_thesis :
     [[ ls = statement_or_thesis;
-       j=justification -> {cut_stat=ls;cut_by=j} ]]
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
   ;
   simple_cut :
     [[ ls = statement;
-       j=justification -> {cut_stat=ls;cut_by=j} ]]
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
   ;
   elim_type:
     [[ IDENT "induction" -> ET_Induction
@@ -76,10 +84,15 @@ GLOBAL: proof_instr;
   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)]]
+    [[ IDENT "consider" ; 
+       h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
+     | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)
+     | IDENT "suffices"; ls=suff_clause;
+       j = justification_items;
+       taco = justification_method 	
+	-> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] 
   ;
   rew_step :
     [[ "~=" ;         c=simple_cut -> (Rhs,c)       
@@ -106,46 +119,112 @@ GLOBAL: proof_instr;
     [[ id=loc_id -> id None ;
      | id=loc_id ; ":" ; c=constr -> id (Some c)]]
   ;
-  vars:
+  consider_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; ","; v=consider_vars -> (Hvar name) :: v
      | name=hyp; 
-       IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h
+       IDENT "such"; IDENT "that"; h=consider_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
+  consider_hyps:  
+    [[ st=statement; IDENT "and"; h=consider_hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; 
+       IDENT "consider" ; v=consider_vars  -> Hprop st::v
      | st=statement -> [Hprop st]
      ]]
+  ;  
+  assume_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=assume_vars -> (Hvar name) :: v
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h
+     ]]
   ;
-  vars_or_thesis:
+  assume_hyps:  
+    [[ st=statement; IDENT "and"; h=assume_hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; 
+       IDENT "we"; IDENT "have" ; v=assume_vars  -> Hprop st::v
+     | st=statement -> [Hprop st]
+     ]]
+  ;
+  assume_clause:
+    [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v
+    |  h=assume_hyps -> h ]]
+  ; 
+  suff_vars:
+    [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
+      [Hvar name],c
+     | name=hyp; ","; v=suff_vars -> 
+	 let (q,c) = v in ((Hvar name) :: q),c
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=suff_hyps -> 
+	 let (q,c) = h in ((Hvar name) :: q),c
+     ]];
+  suff_hyps:  
+    [[ st=statement; IDENT "and"; h=suff_hyps  ->	 
+	 let (q,c) = h in (Hprop st::q),c
+     | st=statement; IDENT "and"; 
+       IDENT "to" ; IDENT "have" ; v=suff_vars -> 
+	 let (q,c) = v in (Hprop st::q),c
+     | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> 
+	 [Hprop st],c
+     ]]
+  ;
+  suff_clause:
+    [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v
+    |  h=suff_hyps -> h ]]
+  ; 
+  let_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=let_vars -> (Hvar name) :: v
+     | name=hyp; IDENT "be"; 
+       IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h
+     ]]
+  ;
+  let_hyps:  
+    [[ st=statement; IDENT "and"; h=let_hyps  -> Hprop st::h
+    |  st=statement; IDENT "and"; "let"; v=let_vars  -> Hprop st::v
+    |  st=statement -> [Hprop st]
+    ]];
+  given_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=given_vars -> (Hvar name) :: v
+     | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h
+     ]]
+  ;
+  given_hyps:  
+    [[ st=statement; IDENT "and"; h=given_hyps  -> Hprop st::h
+    |  st=statement; IDENT "and"; IDENT "given"; v=given_vars  -> Hprop st::v
+    |  st=statement -> [Hprop st]
+    ]];
+  suppose_vars:
     [[name=hyp -> [Hvar name] 
-     |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v
+     |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v
      |name=hyp; OPT[IDENT "be"]; 
-      IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (Hvar name)::h
+      IDENT "such"; IDENT "that"; h=suppose_hyps -> (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];
+  suppose_hyps:  
+    [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h
+     | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have";
+          v=suppose_vars -> Hprop st::v
+     | st=statement_or_thesis -> [Hprop st]
      ]]
   ;
+  suppose_clause:
+    [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v;
+     |  h=suppose_hyps -> h ]]
+  ;
   intro_step:
-    [[ IDENT "suppose" ; h=hyps -> Psuppose h
+    [[ IDENT "suppose" ; h=assume_clause -> 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 ] -> 
+       ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
 	 Pcase (none_is_empty po,c,none_is_empty ho)
-     | "let" ; v=vars -> Plet v	 
+     | "let" ; v=let_vars -> Plet v	 
      | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
-     | IDENT "assume"; h=hyps -> Passume h
-     | IDENT "given"; h=vars -> Pgiven h
+     | IDENT "assume"; h=assume_clause -> Passume h
+     | IDENT "given"; h=given_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)
diff --git a/parsing/g_natsyntaxnew.mli b/parsing/g_natsyntaxnew.mli
deleted file mode 100644
index 97fb8791..00000000
--- a/parsing/g_natsyntaxnew.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id: g_natsyntaxnew.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
-(* Nice syntax for naturals. *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index cba2e7d0..a80d3075 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_tactic.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: g_tactic.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 open Pp
 open Pcoq
@@ -309,6 +309,7 @@ GEXTEND Gram
       | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
+      | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
       | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9bbdc1d4..9a98df80 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 9306 2006-10-28 18:28:19Z herbelin $ *)
+(* $Id: g_vernac.ml4 9562 2007-01-31 09:00:36Z msozeau $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -264,8 +264,8 @@ GEXTEND Gram
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
-      | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
-      | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) 
+      | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
@@ -459,7 +459,7 @@ GEXTEND Gram
       | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
          pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
 	   let pos = option_map (List.map (fun id -> ExplByName id)) pos in
-	   VernacDeclareImplicits (qid,pos)
+	   VernacDeclareImplicits (true,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
@@ -711,7 +711,7 @@ GEXTEND Gram
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
-         "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
+       "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (true,qid,scl)
 
      | IDENT "Infix"; local = locality;
 	 op = ne_string; ":="; p = global; 
diff --git a/parsing/g_zsyntaxnew.mli b/parsing/g_zsyntaxnew.mli
deleted file mode 100644
index 5168722e..00000000
--- a/parsing/g_zsyntaxnew.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id: g_zsyntaxnew.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
-(* Nice syntax for integers. *)
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 7e57885c..bb0662da 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Util 
 open Pp
@@ -22,13 +22,17 @@ let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () 
 
-let pr_justification env = function
-    Automated [] -> mt ()
-  | Automated (_::_ as l) -> 
+let pr_justification_items env = function
+    Some [] -> mt ()
+  | Some (_::_ 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
+  | None -> spc () ++ str "by *"
+
+let pr_justification_method env = function
+    None -> mt ()
+  | Some tac -> 
+      spc () ++ str "using" ++  pr_tac env tac
 
 let pr_statement pr_it env st = 
   pr_label st.st_label ++ pr_it env st.st_it
@@ -41,8 +45,9 @@ let pr_or_thesis pr_this env = function
   | 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
+  hov 1 (pr_it env c.cut_stat) ++ 
+    pr_justification_items env c.cut_by ++
+    pr_justification_method env c.cut_using
 
 let type_or_thesis = function
     Thesis _ -> Term.mkProp
@@ -50,24 +55,24 @@ let type_or_thesis = function
 
 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
+let rec print_hyps pconstr gtyp env sep _be _have hyps = 
+  let pr_sep = if sep 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
+	  spc () ++ pr_sep ++ str _have ++ 
+	    print_vars pconstr gtyp env false _be _have 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
+	      spc() ++ pr_sep ++ pr_statement pconstr env st ++ 
+		print_hyps pconstr gtyp nenv true _be _have rest
 	  end
       | [] -> mt ()
 
-and print_vars pconstr gtyp env _and _be vars =
+and print_vars pconstr gtyp env sep _be _have vars =
   match vars with
     Hvar st :: rest -> 
       begin
@@ -75,26 +80,30 @@ and print_vars pconstr gtyp env _and _be vars =
 	  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 ++
+	let pr_sep = if sep then pr_coma () else mt () in
+		spc() ++ pr_sep ++
 		   pr_statement pr_constr env st ++
-		  print_vars pconstr gtyp nenv true _be rest
+		  print_vars pconstr gtyp nenv true _be _have 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
+	spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
   | [] -> mt ()
 
+let pr_suffices_clause env (hyps,c) = 
+    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
+       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
+
 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
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
 
 let pr_side = function
     Lhs -> str "=~"
@@ -109,30 +118,32 @@ let rec pr_bare_proof_instr _then _thus env = function
       begin
 	match _then,_thus with
 	    false,false -> str "have" ++ spc () ++ 
-	      pr_cut (pr_or_thesis pr_constr) env c
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 	  | false,true  -> str "thus" ++ spc () ++ 
-	      pr_cut (pr_or_thesis pr_constr) env c
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 	  | true,false  -> str "then" ++ spc () ++
-	      pr_cut (pr_or_thesis pr_constr) env c
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 	  | true,true   -> str "hence" ++ spc () ++ 
-	      pr_cut (pr_or_thesis pr_constr) env c
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
       end
+  | Psuffices c ->
+      str "suffices" ++  pr_cut pr_suffices_clause env c 
   | Prew (sid,c) ->
       (if _thus then str "thus" else str "    ") ++ spc () ++
-	pr_side sid ++ spc () ++ pr_cut pr_constr env c
+	pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
   | Passume hyps -> 
-      str "assume" ++ print_hyps pr_constr _I env false false hyps
+      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
   | Plet hyps -> 
-      str "let" ++ print_vars pr_constr _I env false true hyps
+      str "let" ++ print_vars pr_constr _I env false true "let" 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 
+      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps 
       ++ spc () ++ str "from " ++ pr_constr env id 
   | Pgiven hyps ->
-      str "given" ++ print_vars pr_constr _I env false false hyps
+      str "given" ++ print_vars pr_constr _I env false false "given" hyps
   | Ptake witl -> 
       str "take" ++ spc () ++ 
 	prlist_with_sep pr_coma (pr_constr env) witl
@@ -148,7 +159,7 @@ let rec pr_bare_proof_instr _then _thus env = function
 	str "as" ++ (pr_constr env typ)  
   | Psuppose hyps -> 
       str "suppose" ++ 
-	print_hyps pr_constr _I env false false hyps
+	print_hyps pr_constr _I env false false "we have" hyps
   | Pcase (params,pat,hyps) ->
       str "suppose it is" ++ spc () ++ pr_pat pat ++
 	(if params = [] then mt () else 
@@ -160,7 +171,7 @@ let rec pr_bare_proof_instr _then _thus env = function
 	(if hyps = [] then mt () else 
 	   (spc () ++ str "and" ++ 
 	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
-	      env false false hyps))
+	      env false false "we have" hyps))
   | Pper (et,c) -> 
       str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
       pr_casee env c
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c7e1db60..c68a2d6f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *)
+(* $Id: pptactic.ml 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 open Pp
 open Names
@@ -652,6 +652,7 @@ and pr_atom1 = function
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
+  | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f86b5708..f9b8c425 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 9154 2006-09-20 17:18:18Z corbinea $ *)  
+(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *)  
 
 open Pp
 open Names
@@ -447,7 +447,7 @@ let rec pr_vernac = function
   | VernacBindScope (sc,cll) ->
       str"Bind Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll
-  | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function 
+  | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function 
       |	None -> str"_"
       |	Some sc -> str sc in 
     str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
@@ -570,11 +570,11 @@ let rec pr_vernac = function
 			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
 			  else mt()
 		      | CWfRec c -> 
-			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
-			    pr_lconstr_expr c ++ str"}"
+			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ 
+			    pr_name name ++ str"}"
 		      | CMeasureRec c -> 
-			  spc() ++ str "{measure " ++ pr_name name ++ spc() ++ 
-			    pr_lconstr_expr c ++ str"}"
+			  spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ 
+			    pr_name name ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -741,11 +741,11 @@ let rec pr_vernac = function
         (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
          pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (q,None) ->
+  | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (q,Some l) ->
+  | VernacDeclareImplicits (local,q,Some l) ->
       let r = Nametab.global q in
-      Impargs.declare_manual_implicits r l;
+      Impargs.declare_manual_implicits local r l;
       let imps = Impargs.implicits_of_global r in
       hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
              str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c0a98809..6fb492ae 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 9164 2006-09-23 09:36:05Z herbelin $ *)
+(* $Id: printer.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 open Pp
 open Util
@@ -29,7 +29,11 @@ open Pfedit
 open Ppconstr
 open Constrextern
 
-let emacs_str s = if !Options.print_emacs then s else "" 
+let emacs_str s alts = 
+  match !Options.print_emacs, !Options.print_emacs_safechar with
+    | true, true -> alts
+    | true , false -> s
+    | false,_ -> "" 
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -210,7 +214,7 @@ let pr_context_limit n env =
 	   else
              let pidt = pr_var_decl env d in
 	     (i+1, (pps ++ fnl () ++
-		      str (emacs_str (String.make 1 (Char.chr 253))) ++
+		      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 		      pidt)))
         env ~init:(0,(mt ())) 
     in
@@ -219,7 +223,7 @@ let pr_context_limit n env =
         (fun env d pps ->
            let pnat = pr_rel_decl env d in
 	   (pps ++ fnl () ++
-	      str (emacs_str (String.make 1 (Char.chr 253))) ++
+	      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 	      pnat))
         env ~init:(mt ())
     in 
@@ -231,25 +235,15 @@ let pr_context_of env = match Options.print_hyps_limit () with
 
 (* 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
+      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 preamb,penv,pc =
@@ -258,14 +252,14 @@ let pr_goal g =
 	  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
+      let {pm_subgoals=metas} = get_info g in
 	(str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
-    pr_restricted_named_context among env,
+    pr_context_of env,
     pr_subgoal_metas metas env
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (emacs_str (String.make 1 (Char.chr 253)))  ++
+		       str (emacs_str (String.make 1 (Char.chr 253)) "")  ++
 		       str "============================" ++ fnl ()  ++
 		       str" "  ++ pc) ++ fnl ()
      
@@ -273,7 +267,7 @@ let pr_goal g =
 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 (emacs_str (String.make 1 (Char.chr 253)) "")  ++
       str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 
@@ -425,6 +419,13 @@ let pr_prim_rule = function
   | Rename (id1,id2) ->
       (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
 
+  | 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"
+
+
 (* Backwards compatibility *)
 
 let prterm = pr_lconstr
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 6795889c..86af523f 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 9249 2006-10-19 07:46:03Z herbelin $ i*)
+(*i $Id: printer.mli 9385 2006-11-17 15:14:14Z courtieu $ i*)
 
 (*i*)
 open Pp
@@ -98,8 +98,11 @@ val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
 (* Emacs/proof general support *)
-
-val emacs_str              : string -> string
+(* (emacs_str s alts) outputs 
+   - s if emacs mode & unicode allowed, 
+   - alts if emacs mode and & unicode not allowed
+   - nothing otherwise *)
+val emacs_str              : string -> string -> string
 
 (* Backwards compatibility *)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 23d24497..23787f4c 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 9315 2006-10-29 21:53:30Z barras $ *)
+(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 open Util
 open Names
@@ -271,6 +271,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
   | Tacexpr.TacExactNoCheck c ->
       <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
+  | Tacexpr.TacVmCastNoCheck c ->
+      <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply cb ->
       <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (cb,cbo) ->
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 6ea1c97e..1fef688c 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 9244 2006-10-16 17:11:44Z barras $ *)
+(* $Id: tactic_printer.ml 9593 2007-02-05 13:58:52Z corbinea $ *)
 
 open Pp
 open Util
@@ -39,11 +39,6 @@ let pr_rule = function
       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
@@ -51,7 +46,7 @@ let uses_default_tac = function
 
 (* Does not print change of evars *)
 let pr_rule_dot = function 
-  | Change_evars -> mt ()
+  | Prim Change_evars -> mt ()
   | r ->
       pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
@@ -93,7 +88,10 @@ let rec print_decl_script tac_printer nochange sigma pf =
 	 else 
 	   pr_change pf.goal)
 	++ fnl ()
-    | Some (Daimon,_) -> mt ()
+    | Some (Daimon,[]) -> mt ()
+    | Some (Prim Change_evars,[next]) -> 
+      (* ignore evar changes *)
+        print_decl_script tac_printer nochange sigma next
     | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
 	begin
 	  match instr.instr,subprfs with
@@ -213,8 +211,6 @@ let rec print_info_script sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None -> (mt ())
-    | Some(Change_evars,[spf]) ->
-        print_info_script sigma osign spf
     | Some(r,spfl) ->
         (pr_rule r ++ 
            match spfl with