"suffices" implemented + syntax cleanup

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

8 files changed, 260 insertions, 120 deletions

diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 9f9a7e68dd..a8d5fc2ef3 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -81,7 +81,7 @@ let ground_tac solver startseq gl=
 			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
 			    else
 			      backtrack in
-			    forall_tac backtrack continue (re_add seq1)
+			    forall_tac backtrack1 continue (re_add seq1)
 		      | Rarrow->
 			  arrow_tac backtrack continue (re_add seq1)
 		      | Ror->
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index d93350fa59..5c7b40afb7 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
@@ -84,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)       
@@ -114,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
+     ]]
+  ;
+  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
+     ]]
   ;
-  vars_or_thesis:
+  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/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 6e1944b2c2..ec8523d4d3 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -45,7 +45,7 @@ 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) ++ 
+  hov 1 (pr_it env c.cut_stat) ++ 
     pr_justification_items env c.cut_by ++
     pr_justification_method env c.cut_using
 
@@ -55,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
@@ -80,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 "=~"
@@ -114,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
@@ -153,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 
@@ -165,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/tactic_printer.ml b/parsing/tactic_printer.ml
index 005f804400..f8ba788a16 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -88,7 +88,7 @@ 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,[subpf]) ->   
 	print_decl_script tac_printer nochange sigma subpf
     | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 67a1ea5a64..1c5cc0e746 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -38,7 +38,7 @@ type block_type =
   | B_elim of elim_type
 
 type ('it,'constr,'tac) cut =
-    {cut_stat: 'it statement;
+    {cut_stat: 'it;
      cut_by: 'constr list option;
      cut_using: 'tac option}
 
@@ -48,14 +48,15 @@ type ('var,'constr) hyp =
 
 type ('constr,'tac) casee = 
     Real of 'constr 
-  | Virtual of ('constr,'constr,'tac) cut
+  | Virtual of ('constr statement,'constr,'tac) cut
 
 type ('hyp,'constr,'pat,'tac) bare_proof_instr =
   | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
   | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
   | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pcut of ('constr or_thesis,'constr,'tac) cut
-  | Prew of side * ('constr,'constr,'tac) cut
+  | Pcut of ('constr or_thesis statement,'constr,'tac) cut
+  | Prew of side * ('constr statement,'constr,'tac) cut
+  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
   | Passume of ('hyp,'constr) hyp list
   | Plet of ('hyp,'constr) hyp list
   | Pgiven of ('hyp,'constr) hyp list
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 2e54f37438..5428166a99 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -68,9 +68,9 @@ type stack_info =
 
 type pm_info =
     { pm_last: (Names.identifier * bool) option (* anonymous if none *);
-      pm_partial_goal : constr ; (* partial goal construction *)
+      pm_partial_goal : constr; (* partial goal construction *)
       pm_subgoals : (metavariable*constr) list;
-      pm_stack : stack_info list }
+      pm_stack : stack_info list}
 
 let pm_in,pm_out = Dyn.create "pm_info" 
 
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 209d5f52f9..466596d24a 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -20,6 +20,8 @@ open Rawterm
 open Term
 open Pp
 
+(* INTERN *)
+
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
 let intern_justification_items globs = 
@@ -55,13 +57,13 @@ let intern_hyps iconstr globs hyps =
   snd (list_fold_map (intern_hyp iconstr) globs hyps)
 
 let intern_cut intern_it globs cut=
- {cut_stat=intern_statement intern_it globs cut.cut_stat;
+ {cut_stat=intern_it globs cut.cut_stat;
   cut_by=intern_justification_items globs cut.cut_by;
   cut_using=intern_justification_method globs cut.cut_using}
 
 let intern_casee globs = function 
     Real c -> Real (intern_constr globs c)
-  | Virtual cut -> Virtual (intern_cut intern_constr globs cut) 
+  | Virtual cut -> Virtual (intern_cut (intern_statement intern_constr) globs cut) 
 
 let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
@@ -69,6 +71,10 @@ let intern_hyp_list args globs =
     (loc,(id,option_map (intern_constr globs) opttyp)) in
   list_fold_map intern_one globs args 
 
+let intern_suffices_clause globs (hyps,c) = 
+  let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
+    (nhyps,intern_constr_or_thesis nglobs c) 
+
 let intern_fundecl args body globs= 
   let nglobs,nargs = intern_hyp_list args globs in
     nargs,intern_constr nglobs body
@@ -92,8 +98,10 @@ let rec intern_bare_proof_instr globs = function
     Pthus i -> Pthus (intern_bare_proof_instr globs i)
   | Pthen i -> Pthen (intern_bare_proof_instr globs i)
   | Phence i -> Phence (intern_bare_proof_instr globs i)
-  | Pcut c -> Pcut (intern_cut intern_constr_or_thesis globs c) 
-  | Prew (s,c) -> Prew (s,intern_cut intern_constr globs c) 
+  | Pcut c -> Pcut (intern_cut (intern_statement intern_constr_or_thesis) globs c)
+  | Psuffices c -> 
+      Psuffices (intern_cut intern_suffices_clause globs c)
+  | Prew (s,c) -> Prew (s,intern_cut (intern_statement intern_constr) globs c) 
   | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
   | Pcase (params,pat,hyps) -> 
       let nglobs,nparams = intern_hyp_list params globs in
@@ -121,14 +129,16 @@ let rec intern_proof_instr globs instr=
   {emph = instr.emph;
    instr = intern_bare_proof_instr globs instr.instr}
 
-let interp_justification_items env sigma  =
-    option_map (List.map (fun c ->understand env sigma (fst c)))
+(* INTERP *)
 
-let interp_constr check_sort env sigma c = 
+let interp_justification_items sigma env =
+    option_map (List.map (fun c ->understand sigma env (fst c)))
+
+let interp_constr check_sort sigma env c = 
   if check_sort then 
-    understand_type env sigma (fst c) 
+    understand_type sigma env (fst c) 
   else 
-    understand env sigma (fst c)
+    understand sigma env (fst c)
 
 let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
@@ -154,16 +164,16 @@ let get_eq_typ info env =
   let typ = decompose_eq env last_id in  
     typ
 
-let interp_constr_in_type typ env sigma c =
-  understand env sigma (fst c) ~expected_type:typ
+let interp_constr_in_type typ sigma env c =
+  understand sigma env (fst c) ~expected_type:typ
 
-let interp_statement interp_it env sigma st =
+let interp_statement interp_it sigma env st =
   {st_label=st.st_label;
-   st_it=interp_it env sigma st.st_it}
+   st_it=interp_it sigma env st.st_it}
 	
-let interp_constr_or_thesis check_sort env sigma = function
+let interp_constr_or_thesis check_sort sigma env = function
     Thesis n -> Thesis n
-  | This c -> This (interp_constr check_sort env sigma c)
+  | This c -> This (interp_constr check_sort sigma env c)
 
 let type_tester_var body typ = 
   raw_app(dummy_loc,
@@ -179,11 +189,13 @@ let abstract_one_hyp inject h raw =
     | Hprop st -> 
 	RProd (dummy_loc,st.st_label,inject st.st_it, raw)
 
-let rawconstr_of_hyps inject hyps = 
-  List.fold_right (abstract_one_hyp inject) hyps (RSort (dummy_loc,RProp Null))
+let rawconstr_of_hyps inject hyps head = 
+  List.fold_right (abstract_one_hyp inject) hyps head
+
+let raw_prop = RSort (dummy_loc,RProp Null)
   
 let rec match_hyps blend names constr = function 
-    [] -> []
+    [] -> [],constr
   | hyp::q -> 
       let (name,typ,body)=destProd constr in
       let st= {st_label=name;st_it=substl names typ} in
@@ -194,13 +206,14 @@ let rec match_hyps blend names constr = function
       let qhyp = match hyp with
 	  Hprop st' -> Hprop (blend st st')
 	| Hvar _ -> Hvar st in
-	qhyp::(match_hyps blend qnames body q)
+      let rhyps,head = match_hyps blend qnames body q in
+	qhyp::rhyps,head
 
-let interp_hyps_gen inject blend env sigma hyps = 
-  let constr=understand env sigma (rawconstr_of_hyps inject hyps) in
+let interp_hyps_gen inject blend sigma env hyps head = 
+  let constr=understand sigma env (rawconstr_of_hyps inject hyps head) in
     match_hyps blend [] constr hyps
 
-let interp_hyps = interp_hyps_gen fst (fun x _ -> x)
+let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop)
 
 let dummy_prefix= id_of_string "__"
 
@@ -302,7 +315,7 @@ let rec match_aliases names constr = function
 
 let detype_ground c = Detyping.detype false [] [] c
 
-let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
+let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
     match info.pm_stack with
 	Per(et,pi,_,_)::_ -> et,pi
@@ -339,7 +352,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	       str " does not occur in pattern.");
 	Rawterm.RSort(dummy_loc,RProp Null)
     | This (c,_) -> c in
-  let term1 = rawconstr_of_hyps inject hyps in
+  let term1 = rawconstr_of_hyps inject hyps raw_prop in
   let loc_ids,npatt =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in 
@@ -356,11 +369,11 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
   let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
   let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
-  let blend  st st' =
+  let blend st st' =
     match st'.st_it with 
 	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} 
       | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = match_hyps blend nam2 (Termops.pop rest1) hyps in
+  let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in
     tparams,{pat_vars=tpatvars;
 	     pat_aliases=taliases;
 	     pat_constr=pat_pat;
@@ -368,14 +381,21 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	     pat_pat=patt;
 	     pat_expr=pat},thyps
 
-let interp_cut interp_it env sigma cut=
+let interp_cut interp_it sigma env cut=
   {cut with 
-    cut_stat=interp_statement interp_it env sigma cut.cut_stat;
-    cut_by=interp_justification_items env sigma cut.cut_by}
-
-let interp_casee env sigma = function 
-    Real c -> Real (understand env sigma (fst c))
-  | Virtual cut -> Virtual (interp_cut (interp_constr true) env sigma cut) 
+    cut_stat=interp_it sigma env cut.cut_stat;
+    cut_by=interp_justification_items sigma env cut.cut_by}
+
+let interp_suffices_clause sigma env (hyps,cot)=
+  match cot with
+      This (c,_) -> 
+	let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc
+    | Thesis (Plain| Sub _) as th  -> interp_hyps sigma env hyps,th
+      | Thesis (For n) -> error "\"thesis for\" is not applicable here"
+ 
+let interp_casee sigma env = function 
+    Real c -> Real (understand sigma env (fst c))
+  | Virtual cut -> Virtual (interp_cut (interp_statement (interp_constr true)) sigma env cut) 
 
 let abstract_one_arg = function
     (loc,(id,None)) ->
@@ -389,21 +409,25 @@ let abstract_one_arg = function
 let rawconstr_of_fun args body = 
   List.fold_right abstract_one_arg args (fst body)
 
-let interp_fun env sigma args body = 
-  let constr=understand env sigma (rawconstr_of_fun args body) in
+let interp_fun sigma env args body = 
+  let constr=understand sigma env (rawconstr_of_fun args body) in
     match_args destLambda [] constr args
 
-let rec interp_bare_proof_instr info sigma env = function
+let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
     Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
   | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
   | Phence i -> Phence (interp_bare_proof_instr info sigma env i)
-  | Pcut c -> Pcut (interp_cut (interp_constr_or_thesis true) sigma env c) 
+  | Pcut c -> Pcut (interp_cut (interp_statement (interp_constr_or_thesis true)) sigma env c) 
+  | Psuffices c ->  
+      Psuffices (interp_cut interp_suffices_clause sigma env c)
+
   | Prew (s,c) -> Prew (s,interp_cut 
-			  (interp_constr_in_type (get_eq_typ info env))
+			  (interp_statement (interp_constr_in_type (get_eq_typ info env)))
 			  sigma env c) 
+
   | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
   | Pcase (params,pat,hyps) -> 
-      let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in 
+      let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in 
 	Pcase (tparams,tpat,thyps)
   | Ptake witl -> 
       Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 3bb6411656..e2e8a19274 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -98,7 +98,7 @@ let set_last cpl gls =
     tclTHEN 
       begin 
 	match info.pm_last with 
-	    Some (lid,false) -> tclTRY (clear [lid])
+	    Some (lid,false) when not (occur_id [] lid info.pm_partial_goal) -> tclTRY (clear [lid])
 	  | _ -> tclIDTAC
       end
       begin
@@ -458,9 +458,8 @@ let mk_stat_or_thesis info = function
 	  [_,c] -> c
 	| _ -> error 
 	    "\"thesis\" is split, please specify which part you refer to."
-			
-let instr_cut mkstat _thus _then cut gls0 = 
-  let info = get_its_info gls0 in
+
+let just_tac _then cut info gls0 =
   let items_tac gls =
     match cut.cut_by with
 	None -> tclIDTAC gls
@@ -478,21 +477,26 @@ let instr_cut mkstat _thus _then cut gls0 =
 	  automation_tac gls
       | Some tac -> 
 	  (Tacinterp.eval_tactic tac) gls in
-  let just_tac gls =
-    justification (tclTHEN items_tac method_tac) gls in
-  let (c_id,_) as cpl = match cut.cut_stat.st_label with 
+    justification (tclTHEN items_tac method_tac) gls0
+			
+let instr_cut mkstat _thus _then cut gls0 = 
+  let info = get_its_info gls0 in 
+  let stat = cut.cut_stat in
+  let (c_id,_) as cpl = match stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_fact") gls0,false 
     | Name id -> id,true in
-  let c_stat = mkstat info cut.cut_stat.st_it in
+  let c_stat = mkstat info stat.st_it in
   let thus_tac gls= 
     if _thus then 
       thus_tac (mkVar c_id) c_stat gls
     else tclIDTAC gls in
     tclTHENS (internal_cut c_id c_stat) 
-      [tclTHEN tcl_erase_info just_tac;
+      [tclTHEN tcl_erase_info (just_tac _then cut info);
        tclTHEN (set_last cpl) thus_tac] gls0
 
+
+
 (* iterated equality *)
 let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
 
@@ -641,6 +645,49 @@ let assume_st_letin hyps gls =
 	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
 	 hyps tclIDTAC gls 
 
+(* suffices *)
+
+let free_meta info = 
+  let max_next (i,_) j  = if i <= j then succ j else i in
+  List.fold_right max_next info.pm_subgoals 1
+
+let rec metas_from n hyps = 
+  match hyps with
+      _ :: q -> mkMeta n :: metas_from (succ n) q
+    | [] -> []
+ 
+let rec build_product args body =
+  match args with 
+      (Hprop st| Hvar st )::rest -> 
+	let pprod= lift 1 (build_product rest body) in
+	let lbody =
+	  match st.st_label with
+	      Anonymous -> body
+	    | Name id -> subst_term (mkVar id) pprod in
+	  mkProd (st.st_label, st.st_it, lbody)
+    | [] -> body 
+
+let instr_suffices _then cut gls0 = 
+  let info = get_its_info gls0 in 
+  let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in 
+  let ctx,hd = cut.cut_stat in
+  let c_stat = build_product ctx (mk_stat_or_thesis info hd) in
+  let metas = metas_from (free_meta info) ctx in
+  let c_costat = prod_applist c_stat metas in
+  let costat = applist (mkVar c_id,metas) in  
+ let thus_tac gls= 
+      thus_tac costat c_costat gls in
+   tclTHENS (internal_cut c_id c_stat) 
+     [tclTHENLIST 
+	 [ tcl_change_info 
+	     {info with 
+	       pm_partial_goal=mkMeta 1;
+	       pm_subgoals=[1,c_stat]};
+	   assume_tac ctx;   
+	   tcl_erase_info;
+	   just_tac _then cut info];
+      tclTHEN (set_last (c_id,false)) thus_tac] gls0
+
 (* tactics for consider/given *)
 
 let update_goal_info gls =
@@ -873,17 +920,6 @@ let per_tac etype casee gls=
 
 (* suppose *)
 
-let rec build_product args body =
-  match args with 
-      (Hprop st| Hvar st )::rest -> 
-	let pprod= lift 1 (build_product rest body) in
-	let lbody =
-	  match st.st_label with
-	      Anonymous -> body
-	    | Name id -> subst_term (mkVar id) pprod in
-	  mkProd (st.st_label, st.st_it, lbody)
-    | [] -> body 
-
 let register_nodep_subcase id= function
     Per(et,pi,ek,clauses)::s ->
       begin
@@ -1411,6 +1447,8 @@ let rec do_proof_instr_gen _thus _then instr =
 	do_proof_instr_gen true true i
     | Pcut c ->
 	instr_cut mk_stat_or_thesis _thus _then c
+    | Psuffices c ->
+	instr_suffices _then c 
     | Prew (s,c) ->
 	assert (not _then);
 	instr_rew _thus s c
@@ -1435,7 +1473,7 @@ let eval_instr {instr=instr} =
 let rec preprocess pts instr =
   match instr with
     Phence i |Pthus i | Pthen i -> preprocess pts i
-  | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
+  | Psuffices _ | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
   | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ 
   | Pdefine (_,_,_) | Pper _ | Prew _ ->
       check_not_per pts;
@@ -1451,7 +1489,7 @@ let rec preprocess pts instr =
 let rec postprocess pts instr = 
   match instr with
       Phence i | Pthus i | Pthen i -> postprocess pts i
-    | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
+    | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
     | Pescape -> escape_command pts