- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses

- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward


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

13 files changed, 365 insertions, 302 deletions

diff --git a/CHANGES b/CHANGES
index cf0d007eab..f6d9aac8a9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,6 +57,8 @@ Tactics
   used to solve unresolved subterms of term arguments of tactics.
 - Better support for coercions to Sortclass in tactics expecting type arguments
 - Low-priority term printer made available in ML-written tactic extensions
+- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
+- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
 
 Modules
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index bd9e1f7f31..9b5c14f239 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1155,17 +1155,23 @@ and xlate_tac =
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
+    | TacLetTac (na, c, cl) when cl = nowhere -> 
+        CT_pose(xlate_id_opt_aux na, xlate_formula c)
     | TacLetTac (na, c, cl) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
-    | TacForward (true, name, c) -> 
-               CT_pose(xlate_id_opt_aux name, xlate_formula c)
-    | TacForward (false, name, c) -> 
-               CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
-    | TacTrueCut (na, c) -> 
-        CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
+    | TacAssert (None, Some (IntroIdentifier id), c) -> 
+        CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (None, None, c) -> 
+        CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert (Some (TacId ""), Some (IntroIdentifier id), c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (Some (TacId ""), None, c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert _ ->
+	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
     | TacAnyConstructor(Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f27191e2ec..f7c05c7786 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -68,6 +68,24 @@ let lpar_id_colon =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let guess_lpar_ipat s strm =
+  match Stream.npeek 1 strm with
+    | [("","(")] ->
+        (match Stream.npeek 2 strm with
+          | [_; ("",("("|"["))] -> ()
+          | [_; ("IDENT",_)] ->
+              (match Stream.npeek 3 strm with
+                | [_; _; ("", s')] when s = s' -> ()
+                | _ -> raise Stream.Failure)
+          | _ -> raise Stream.Failure)
+    | _ -> raise Stream.Failure
+
+let guess_lpar_coloneq =
+  Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=")
+
+let guess_lpar_colon =
+  Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":")
+
 open Constr
 open Prim
 open Tactic
@@ -261,6 +279,9 @@ GEXTEND Gram
   with_names:
     [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ]
   ;
+  by_tactic:
+    [ [ "by"; tac = tactic -> tac | -> TacId "" ] ]
+  ;
   simple_tactic:
     [ [ 
       (* Basic tactics *)
@@ -293,22 +314,30 @@ GEXTEND Gram
       | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
 	  TacMutualCofix (id,List.map mk_cofix_tac fd)
 
-      | IDENT "cut"; c = constr -> TacCut c
-      | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
-          TacTrueCut (Names.Name id,t)
-      | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
-          TacForward (false,Names.Name id,b)
-      | IDENT "assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
-	  TacForward (true,Names.Name id,b)
-      | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
-      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
-      | IDENT "generalize"; IDENT "dependent"; c = constr ->
-          TacGeneralizeDep c
-      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")";
-          p = clause -> TacLetTac (Names.Name id,c,p)
+	  TacLetTac (Names.Name id,b,nowhere)
+      | IDENT "pose"; b = constr ->
+	  TacLetTac (Names.Anonymous,b,nowhere)
+      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")"; p = clause ->
+	  TacLetTac (Names.Name id,c,p)
       | IDENT "set"; c = constr; p = clause ->
           TacLetTac (Names.Anonymous,c,p)
+
+      (* Begin compatibility *)
+      | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
+	  TacAssert (None,Some (IntroIdentifier id),c)
+      | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic -> 
+	  TacAssert (Some tac,Some (IntroIdentifier id),c)
+      (* End compatibility *)
+
+      | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
+	  TacAssert (Some tac,ipat,c)
+      | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names ->
+	  TacAssert (None,ipat,c)
+
+      | IDENT "cut"; c = constr -> TacCut c
+      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
+      | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
     (*  | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; "in";
 	  hid = hypident ->
 	    let (id,(hloc,_)) = hid in
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 46caf88b82..c1eef07dcb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -366,6 +366,30 @@ let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
+let pr_pose prlc prc na c = match na with
+  | Anonymous -> spc() ++ prc c
+  | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+let pr_assertion _prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | Some (IntroIdentifier id) ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_with_names ipat
+
+let pr_assumption prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | Some (IntroIdentifier id) ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_with_names ipat
+
+let pr_by_tactic prt = function
+  | TacId "" -> mt ()
+  | tac -> spc() ++ str "by " ++ prt tac
+
 let pr_occs pp = function
     [] -> pp
   | nl -> hov 1 (pp ++ spc() ++ str"at " ++
@@ -577,7 +601,6 @@ let pr_fix_tac env (id,n,c) =
 let pr_cofix_tac env (id,c) =
   hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
 
-
   (* Printing tactics as arguments *)
 let rec pr_atom0 env = function
   | TacIntroPattern [] -> str "intros"
@@ -632,34 +655,23 @@ and pr_atom1 env = function
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
-  | TacTrueCut (Anonymous,c) -> 
-      hov 1 (str "assert" ++ pr_constrarg env c)
-  | TacTrueCut (Name id,c) -> 
-      hov 1 (str "assert" ++ spc () ++
-             hov 1 (str"(" ++ pr_id id ++ str " :" ++
-                    pr_lconstrarg env c ++ str")"))
-  | TacForward (false,na,c) ->
-      hov 1 (str "assert" ++ spc () ++
-             hov 1 (str"(" ++ pr_name na ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")"))
-  | TacForward (true,Anonymous,c) ->
-      hov 1 (str "pose" ++ pr_constrarg env c)
-  | TacForward (true,Name id,c) ->
-      hov 1 (str "pose" ++ spc() ++
-             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")"))
+  | TacAssert (Some tac,ipat,c) -> 
+      hov 1 (str "assert" ++ 
+             pr_assumption (pr_lconstr env) (pr_constr env) ipat c ++ 
+             pr_by_tactic (pr_tac_level env ltop) tac)
+  | TacAssert (None,ipat,c) -> 
+      hov 1 (str "pose proof" ++
+             pr_assertion (pr_lconstr env) (pr_constr env) ipat c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep spc (pr_constr env) l)
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg env c)
-  | TacLetTac (Anonymous,c,cl) ->
-      hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl
-  | TacLetTac (Name id,c,cl) ->
-      hov 1 (str "set" ++ spc () ++
-             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")") ++
+  | TacLetTac (na,c,cl) when cl = nowhere ->
+      hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c)
+  | TacLetTac (na,c,cl) ->
+      hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++
              pr_clauses pr_ident cl)
 (*  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f8172ac6e1..659f64c7b6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -297,11 +297,10 @@ let rec mlexpr_of_atomic_tactic = function
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
-  | Tacexpr.TacTrueCut (na,c) ->
-      let na = mlexpr_of_name na in
-      <:expr< Tacexpr.TacTrueCut $na$ $mlexpr_of_constr c$ >>
-  | Tacexpr.TacForward (b,na,c) ->
-      <:expr< Tacexpr.TacForward $mlexpr_of_bool b$ $mlexpr_of_name na$ $mlexpr_of_constr c$ >>
+  | Tacexpr.TacAssert (t,ipat,c) ->
+      let ipat = mlexpr_of_option mlexpr_of_intro_pattern ipat in
+      <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
+	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
       <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >>
   | Tacexpr.TacGeneralizeDep c ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8de1e789a..c2b226281c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -84,6 +84,8 @@ type 'id gclause =
     onconcl : bool;
     concl_occs :int list }
 
+let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
+
 let simple_clause_of = function
     { onhyps = Some[scl]; onconcl = false } -> Some scl
   | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
@@ -123,8 +125,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacTrueCut of name * 'constr 
-  | TacForward of bool * name * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr option * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6cdcf1fb5e..6b67dd4966 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1075,8 +1075,9 @@ let subst_one x gl =
   let introtac = function
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
-        forward true (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast,
-                                       replace_term varx rhs htyp))
+        letin_tac true (Name id)
+	  (mkCast(replace_term varx rhs hval,DEFAULTcast,
+	          replace_term varx rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d1a2b40b1c..a321b9f1b9 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,5 +71,5 @@ let let_evar name typ gls =
   let evd = Evd.create_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
   Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
-    (Tactics.forward true name evar) gls
+    (Tactics.letin_tac true name evar nowhere) gls
  
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index d5da2c86b9..73259b5ffa 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -42,8 +42,6 @@ let h_mutual_cofix id l =
   abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l)
 
 let h_cut c          = abstract_tactic (TacCut c) (cut c)
-let h_true_cut na c = abstract_tactic (TacTrueCut (na,c)) (true_cut na c)
-let h_forward b na c = abstract_tactic (TacForward (b,na,c)) (forward b na c)
 let h_generalize cl  = abstract_tactic (TacGeneralize cl) (generalize cl)
 let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
 let h_let_tac na c cl =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 5c375ddce7..3e66391cfc 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -46,10 +46,8 @@ val h_mutual_cofix    : identifier -> (identifier * constr) list -> tactic
 val h_cofix           : identifier option -> tactic
 
 val h_cut             : constr -> tactic 
-val h_true_cut        : name -> constr -> tactic 
 val h_generalize      : constr list -> tactic 
 val h_generalize_dep  : constr -> tactic 
-val h_forward         : bool -> name -> constr -> tactic 
 val h_let_tac         : name -> constr -> Tacticals.clause -> tactic
 val h_instantiate     : int -> Rawterm.rawconstr ->
   (identifier * hyp_location_flag, unit) location -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2442b4aa5b..c3c01f3a2f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -631,10 +631,10 @@ let rec intern_atomic lf ist x =
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
-  | TacTrueCut (na,c) ->
-      TacTrueCut (intern_name lf ist na, intern_type ist c)
-  | TacForward (b,na,c) ->
-      TacForward (b,intern_name lf ist na,intern_constr ist c)
+  | TacAssert (otac,ipat,c) ->
+      TacAssert (option_app (intern_tactic ist) otac,
+                 option_app (intern_intro_pattern lf ist) ipat,
+                 intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
   | TacLetTac (na,c,cls) ->
@@ -1703,10 +1703,11 @@ and interp_atomic ist gl = function
       let f (id,c) = (interp_ident ist id,pf_interp_type ist gl c) in
       h_mutual_cofix (interp_ident ist id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_type ist gl c)
-  | TacTrueCut (na,c) ->
-      h_true_cut (interp_name ist na) (pf_interp_type ist gl c)
-  | TacForward (b,na,c) ->
-      h_forward b (interp_name ist na) (pf_interp_constr ist gl c)
+  | TacAssert (t,ipat,c) ->
+      let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
+      abstract_tactic (TacAssert (t,ipat,c))
+        (Tactics.forward (option_app (interp_tactic ist) t)
+	  (option_app (interp_intro_pattern ist) ipat) c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp) ->
@@ -1975,8 +1976,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
-  | TacTrueCut (ido,c) -> TacTrueCut (ido, subst_rawconstr subst c)
-  | TacForward (b,na,c) -> TacForward (b,na,subst_rawconstr subst c)
+  | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c)
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e383c0c06..2e49cd51a3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -500,6 +500,10 @@ let apply_without_reduce c gl =
   end.
 *)
 
+(**************************)
+(*     Cut tactics        *)
+(**************************)
+
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
   match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
@@ -509,24 +513,6 @@ let cut_and_apply c gl =
 	  (apply_term c [mkMeta (new_meta())]) gl
     | _ -> error "Imp_elim needs a non-dependent product"
 
-(**************************)
-(*     Cut tactics        *)
-(**************************)
-
-let assert_tac first na c gl =
-  match kind_of_term (hnf_type_of gl c) with
-    | Sort s -> 
-	let id = match na with
-	  | Anonymous -> 
-              let d = match s with Prop _ -> "H" | Type _ -> "X" in
-              fresh_id [] (id_of_string d) gl
-	  | Name id -> id
-	in
-	(if first then internal_cut else internal_cut_rev) id c gl
-    | _  -> error "Not a proposition or a type"
-
-let true_cut = assert_tac true
-
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort _ ->
@@ -554,222 +540,6 @@ let cut_in_parallel l =
   in 
   prec (List.rev l)
 
-(**************************)
-(*   Generalize tactics   *)
-(**************************)
-
-let generalize_goal gl c cl =
-  let t = pf_type_of gl c in
-  match kind_of_term c with
-    | Var id ->
-	(* The choice of remembering or not a non dependent name has an impact
-	   on the future Intro naming strategy! *)
-	(* if dependent c cl then mkNamedProd id t cl
-	   else mkProd (Anonymous,t,cl) *)
-	mkNamedProd id t cl
-    | _        -> 
-        let cl' = subst_term c cl in
-        if noccurn 1 cl' then 
-	  mkProd (Anonymous,t,cl)
-          (* On ne se casse pas la tete : on prend pour nom de variable
-             la premiere lettre du type, meme si "ci" est une
-             constante et qu'on pourrait prendre directement son nom *)
-        else 
-	  prod_name (Global.env()) (Anonymous, t, cl')
-
-let generalize_dep c gl =
-  let env = pf_env gl in
-  let sign = pf_hyps gl in
-  let init_ids = ids_of_named_context (Global.named_context()) in
-  let rec seek d toquant =
-    if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
-      or dependent_in_decl c d then 
-      d::toquant
-    else 
-      toquant in
-  let to_quantify = Sign.fold_named_context seek sign ~init:[] in
-  let to_quantify_rev = List.rev to_quantify in
-  let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
-  let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
-  let tothin' =
-    match kind_of_term c with
-      | Var id when mem_named_context id sign & not (List.mem id init_ids)
-	  -> id::tothin
-      | _ -> tothin
-  in
-  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let cl'' = generalize_goal gl c cl' in
-  let args = Array.to_list (instance_from_named_context to_quantify_rev) in
-  tclTHEN
-    (apply_type cl'' (c::args))
-    (thin (List.rev tothin'))
-    gl
-    
-let generalize lconstr gl = 
-  let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in
-  apply_type newcl lconstr gl
-
-(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
-Cela peut-être troublant de faire "Generalize Dependent H n" dans
-"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
-généralisation dépendante par n.
-
-let quantify lconstr =
- List.fold_right 
-   (fun com tac -> tclTHEN tac (tactic_com generalize_dep c))
-   lconstr
-   tclIDTAC
-*)
-
-(* A dependent cut rule à la sequent calculus
-   ------------------------------------------
-   Sera simplifiable le jour où il y aura un let in primitif dans constr
-
-   [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
-   [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
-   [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
-   [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
-
-   [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted;
-   if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted
-   wherever it occurs, otherwise [c] is substituted only in hyps
-   present in [occ_hyps] at the specified occurrences (everywhere if
-   the list of occurrences is empty), and in the goal at the specified
-   occurrences if [occ_goal] is not [None];
-
-   if name = Anonymous, the name is build from the first letter of the type;
-
-   The tactic first quantify the goal over x1, x2,... then substitute then
-   re-intro x1, x2,... at their initial place ([marks] is internally
-   used to remember the place of x1, x2, ...: it is the list of hypotheses on
-   the left of each x1, ...).
-*)
-
-
-
-let occurrences_of_hyp id cls =
-  let rec hyp_occ = function
-      [] -> None
-    | (id',occs,hl)::_ when id=id' -> Some occs
-    | _::l -> hyp_occ l in
-  match cls.onhyps with
-      None -> Some []
-    | Some l -> hyp_occ l
-
-let occurrences_of_goal cls =
-  if cls.onconcl then Some cls.concl_occs else None
-
-let in_every_hyp cls = (cls.onhyps=None)
-
-(*
-(* Implementation with generalisation then re-intro: introduces noise *)
-(* in proofs *)
-
-let letin_abstract id c occs gl =
-  let env = pf_env gl in
-  let compute_dependency _ (hyp,_,_ as d) ctxt =
-    let d' =
-      try
-	match occurrences_of_hyp hyp occs with
-	  | None -> raise Not_found
-	  | Some occ ->
-              let newdecl = subst_term_occ_decl occ c d in
-              if occ = [] & d = newdecl then
-		if not (in_every_hyp occs)
-		then raise (RefinerError (DoesNotOccurIn (c,hyp)))
-		else raise Not_found
-              else 
-		(subst1_decl (mkVar id) newdecl, true)
-	with Not_found -> 
-	  (d,List.exists
-	      (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
-    in d'::ctxt
-  in 
-  let ctxt' = fold_named_context compute_dependency env ~init:[] in
-  let compute_marks ((depdecls,marks as accu),lhyp) ((hyp,_,_) as d,b) =
-    if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp)
-    else (accu, Some hyp) in
-  let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in
-  let ccl = match occurrences_of_goal occs with
-    | None -> pf_concl gl
-    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl))
-  in
-  (depdecls,marks,ccl)
-
-let letin_tac with_eq name c occs gl =
-  let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
-  let id =
-    if name = Anonymous then fresh_id [] x gl else
-      if not (mem_named_context x (pf_hyps gl)) then x else
-	error ("The variable "^(string_of_id x)^" is already declared") in
-  let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
-  let t = pf_type_of gl c in
-  let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let args = Array.to_list (instance_from_named_context depdecls) in
-  let newcl = mkNamedLetIn id c t tmpcl in
-  let lastlhyp = if marks=[] then None else snd (List.hd marks) in
-  tclTHENLIST
-    [ apply_type newcl args;
-      thin (List.map (fun (id,_,_) -> id) depdecls);
-      intro_gen (IntroMustBe id) lastlhyp false;
-      if with_eq then tclIDTAC else thin_body [id];
-      intros_move marks ] gl
-*)
-
-(* Implementation without generalisation: abbrev will be lost in hyps in *)
-(* in the extracted proof *)
-
-let letin_abstract id c occs gl =
-  let env = pf_env gl in
-  let compute_dependency _ (hyp,_,_ as d) depdecls =
-    match occurrences_of_hyp hyp occs with
-      | None -> depdecls
-      | Some occ ->
-          let newdecl = subst_term_occ_decl occ c d in
-          if occ = [] & d = newdecl then
-	    if not (in_every_hyp occs)
-	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
-	    else depdecls
-          else 
-	    (subst1_decl (mkVar id) newdecl)::depdecls in 
-  let depdecls = fold_named_context compute_dependency env ~init:[] in
-  let ccl = match occurrences_of_goal occs with
-    | None -> pf_concl gl
-    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in
-  let lastlhyp = if depdecls = [] then None else Some(pi1(list_last depdecls)) in
-  (depdecls,lastlhyp,ccl)
-
-let letin_tac with_eq name c occs gl =
-  let id =
-    let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
-    if name = Anonymous then fresh_id [] x gl else
-      if not (mem_named_context x (pf_hyps gl)) then x else
-	error ("The variable "^(string_of_id x)^" is already declared") in
-  let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = refresh_universes (pf_type_of gl c) in
-  let newcl = mkNamedLetIn id c t ccl in
-  tclTHENLIST
-    [ convert_concl_no_check newcl DEFAULTcast;
-      intro_gen (IntroMustBe id) lastlhyp true;
-      if with_eq then tclIDTAC else thin_body [id];
-      tclMAP convert_hyp_no_check depdecls ] gl
-  
-let check_hypotheses_occurrences_list env (_,occl) =
-  let rec check acc = function
-    | (hyp,_) :: rest -> 
-	if List.mem hyp acc then
-	  error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
-	if not (mem_named_context hyp (named_context env)) then
-	  error ("No such hypothesis: " ^ (string_of_id hyp));
-	check (hyp::acc) rest
-    | [] -> ()
-  in check [] occl
-
-let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
-
-(* Tactics "assert (...:=...)" (b=false) and "pose" (b=true) *)
-let forward b na c = letin_tac b na c nowhere
-
 (********************************************************************)
 (*               Exact tactics                                      *)
 (********************************************************************)
@@ -1063,6 +833,252 @@ let intro_patterns = function
   | [] -> tclREPEAT intro
   | l  -> intros_pattern None l
 
+(**************************)
+(*   Other cut tactics    *)
+(**************************)
+
+let hid = id_of_string "H"
+let xid = id_of_string "X"
+
+let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
+
+let prepare_intros s ipat gl = match ipat with
+  | None -> make_id s gl, tclIDTAC
+  | Some IntroWildcard -> let id = make_id s gl in id, thin [id]
+  | Some (IntroIdentifier id) -> id, tclIDTAC
+  | Some (IntroOrAndPattern ll) -> make_id s gl, 
+        (tclTHENS 
+	  (tclTHEN case_last clear_last)
+	  (List.map (intros_patterns [] None) ll))
+
+let ipat_of_name = function
+  | Anonymous -> None
+  | Name id -> Some (IntroIdentifier id)
+
+let assert_as first ipat c gl =
+  match kind_of_term (hnf_type_of gl c) with
+  | Sort s ->
+      let id,tac = prepare_intros s ipat gl in
+      tclTHENS ((if first then internal_cut else internal_cut_rev) id c)
+	(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
+  | _  -> error "Not a proposition or a type"
+
+let assert_tac first na = assert_as first (ipat_of_name na)
+let true_cut = assert_tac true 
+
+(**************************)
+(*   Generalize tactics   *)
+(**************************)
+
+let generalize_goal gl c cl =
+  let t = pf_type_of gl c in
+  match kind_of_term c with
+    | Var id ->
+	(* The choice of remembering or not a non dependent name has an impact
+	   on the future Intro naming strategy! *)
+	(* if dependent c cl then mkNamedProd id t cl
+	   else mkProd (Anonymous,t,cl) *)
+	mkNamedProd id t cl
+    | _        -> 
+        let cl' = subst_term c cl in
+        if noccurn 1 cl' then 
+	  mkProd (Anonymous,t,cl)
+          (* On ne se casse pas la tete : on prend pour nom de variable
+             la premiere lettre du type, meme si "ci" est une
+             constante et qu'on pourrait prendre directement son nom *)
+        else 
+	  prod_name (Global.env()) (Anonymous, t, cl')
+
+let generalize_dep c gl =
+  let env = pf_env gl in
+  let sign = pf_hyps gl in
+  let init_ids = ids_of_named_context (Global.named_context()) in
+  let rec seek d toquant =
+    if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
+      or dependent_in_decl c d then 
+      d::toquant
+    else 
+      toquant in
+  let to_quantify = Sign.fold_named_context seek sign ~init:[] in
+  let to_quantify_rev = List.rev to_quantify in
+  let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
+  let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
+  let tothin' =
+    match kind_of_term c with
+      | Var id when mem_named_context id sign & not (List.mem id init_ids)
+	  -> id::tothin
+      | _ -> tothin
+  in
+  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
+  let cl'' = generalize_goal gl c cl' in
+  let args = Array.to_list (instance_from_named_context to_quantify_rev) in
+  tclTHEN
+    (apply_type cl'' (c::args))
+    (thin (List.rev tothin'))
+    gl
+    
+let generalize lconstr gl = 
+  let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in
+  apply_type newcl lconstr gl
+
+(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
+Cela peut-être troublant de faire "Generalize Dependent H n" dans
+"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
+généralisation dépendante par n.
+
+let quantify lconstr =
+ List.fold_right 
+   (fun com tac -> tclTHEN tac (tactic_com generalize_dep c))
+   lconstr
+   tclIDTAC
+*)
+
+(* A dependent cut rule à la sequent calculus
+   ------------------------------------------
+   Sera simplifiable le jour où il y aura un let in primitif dans constr
+
+   [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
+   [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
+   [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
+   [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
+
+   [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted;
+   if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted
+   wherever it occurs, otherwise [c] is substituted only in hyps
+   present in [occ_hyps] at the specified occurrences (everywhere if
+   the list of occurrences is empty), and in the goal at the specified
+   occurrences if [occ_goal] is not [None];
+
+   if name = Anonymous, the name is build from the first letter of the type;
+
+   The tactic first quantify the goal over x1, x2,... then substitute then
+   re-intro x1, x2,... at their initial place ([marks] is internally
+   used to remember the place of x1, x2, ...: it is the list of hypotheses on
+   the left of each x1, ...).
+*)
+
+
+
+let occurrences_of_hyp id cls =
+  let rec hyp_occ = function
+      [] -> None
+    | (id',occs,hl)::_ when id=id' -> Some occs
+    | _::l -> hyp_occ l in
+  match cls.onhyps with
+      None -> Some []
+    | Some l -> hyp_occ l
+
+let occurrences_of_goal cls =
+  if cls.onconcl then Some cls.concl_occs else None
+
+let in_every_hyp cls = (cls.onhyps=None)
+
+(*
+(* Implementation with generalisation then re-intro: introduces noise *)
+(* in proofs *)
+
+let letin_abstract id c occs gl =
+  let env = pf_env gl in
+  let compute_dependency _ (hyp,_,_ as d) ctxt =
+    let d' =
+      try
+	match occurrences_of_hyp hyp occs with
+	  | None -> raise Not_found
+	  | Some occ ->
+              let newdecl = subst_term_occ_decl occ c d in
+              if occ = [] & d = newdecl then
+		if not (in_every_hyp occs)
+		then raise (RefinerError (DoesNotOccurIn (c,hyp)))
+		else raise Not_found
+              else 
+		(subst1_decl (mkVar id) newdecl, true)
+	with Not_found -> 
+	  (d,List.exists
+	      (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
+    in d'::ctxt
+  in 
+  let ctxt' = fold_named_context compute_dependency env ~init:[] in
+  let compute_marks ((depdecls,marks as accu),lhyp) ((hyp,_,_) as d,b) =
+    if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp)
+    else (accu, Some hyp) in
+  let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in
+  let ccl = match occurrences_of_goal occs with
+    | None -> pf_concl gl
+    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl))
+  in
+  (depdecls,marks,ccl)
+
+let letin_tac with_eq name c occs gl =
+  let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
+  let id =
+    if name = Anonymous then fresh_id [] x gl else
+      if not (mem_named_context x (pf_hyps gl)) then x else
+	error ("The variable "^(string_of_id x)^" is already declared") in
+  let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
+  let t = pf_type_of gl c in
+  let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
+  let args = Array.to_list (instance_from_named_context depdecls) in
+  let newcl = mkNamedLetIn id c t tmpcl in
+  let lastlhyp = if marks=[] then None else snd (List.hd marks) in
+  tclTHENLIST
+    [ apply_type newcl args;
+      thin (List.map (fun (id,_,_) -> id) depdecls);
+      intro_gen (IntroMustBe id) lastlhyp false;
+      if with_eq then tclIDTAC else thin_body [id];
+      intros_move marks ] gl
+*)
+
+(* Implementation without generalisation: abbrev will be lost in hyps in *)
+(* in the extracted proof *)
+
+let letin_abstract id c occs gl =
+  let env = pf_env gl in
+  let compute_dependency _ (hyp,_,_ as d) depdecls =
+    match occurrences_of_hyp hyp occs with
+      | None -> depdecls
+      | Some occ ->
+          let newdecl = subst_term_occ_decl occ c d in
+          if occ = [] & d = newdecl then
+	    if not (in_every_hyp occs)
+	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
+	    else depdecls
+          else 
+	    (subst1_decl (mkVar id) newdecl)::depdecls in 
+  let depdecls = fold_named_context compute_dependency env ~init:[] in
+  let ccl = match occurrences_of_goal occs with
+    | None -> pf_concl gl
+    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in
+  let lastlhyp = if depdecls = [] then None else Some(pi1(list_last depdecls)) in
+  (depdecls,lastlhyp,ccl)
+
+let letin_tac with_eq name c occs gl =
+  let id =
+    let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
+    if name = Anonymous then fresh_id [] x gl else
+      if not (mem_named_context x (pf_hyps gl)) then x else
+	error ("The variable "^(string_of_id x)^" is already declared") in
+  let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
+  let t = refresh_universes (pf_type_of gl c) in
+  let newcl = mkNamedLetIn id c t ccl in
+  tclTHENLIST
+    [ convert_concl_no_check newcl DEFAULTcast;
+      intro_gen (IntroMustBe id) lastlhyp true;
+      if with_eq then tclIDTAC else thin_body [id];
+      tclMAP convert_hyp_no_check depdecls ] gl
+  
+(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
+let forward usetac ipat c gl =
+  match usetac with
+  | None -> 
+      let t = refresh_universes (pf_type_of gl c) in
+      tclTHENS (assert_as true ipat t) [exact_no_check c; tclIDTAC] gl
+  | Some tac -> 
+      tclTHENS (assert_as true ipat c) [tac; tclIDTAC] gl
+
+(*****************************)
+(* High-level induction      *)
+(*****************************)
+
 (*
  * A "natural" induction tactic
  * 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 91c6731b7a..95a2facc07 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -239,10 +239,11 @@ val cut_replacing               :
   identifier -> constr -> (tactic -> tactic) -> tactic
 val cut_in_parallel             : constr list -> tactic
 
-val assert_tac                  : bool -> name -> constr -> tactic
+val assert_as : bool -> intro_pattern_expr option -> constr -> tactic
 val true_cut                    : name -> constr -> tactic
 val letin_tac                   : bool -> name -> constr -> clause -> tactic
-val forward                     : bool -> name -> constr -> tactic
+val assert_tac                  : bool -> name -> constr -> tactic
+val forward    : tactic option -> intro_pattern_expr option -> constr -> tactic
 val generalize                  : constr list -> tactic
 val generalize_dep              : constr  -> tactic