Merge branch 'clean-atomic-tactics'

4 files changed, 69 insertions, 98 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 63fb67e146..74d98176a4 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -15,6 +15,7 @@ open Misctypes
 open Genredexpr
 
 open Proofview.Notations
+open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
 
@@ -140,10 +141,19 @@ END
 
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
+| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ]
 END
 
 (** Split *)
 
+let rec delayed_list = function
+| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma }
+| x :: l ->
+  { Tacexpr.delayed = fun env sigma ->
+    let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in
+    let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in
+    Sigma (x :: l, sigma, p +> q) }
+
 TACTIC EXTEND split
   [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
 END
@@ -164,12 +174,35 @@ TACTIC EXTEND esplit_with
   ]
 END
 
+TACTIC EXTEND exists
+  [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [
+    Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
+  ]
+END
+
+TACTIC EXTEND eexists
+  [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [
+    Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
+  ]
+END
+
 (** Intro *)
 
 TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 END
 
+(** Move *)
+
+TACTIC EXTEND move
+  [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ]
+| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ]
+| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ]
+| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ]
+END
+
 (** Revert *)
 
 TACTIC EXTEND revert
@@ -192,6 +225,42 @@ TACTIC EXTEND admit
  [ "admit" ] -> [ Proofview.give_up ]
 END
 
+(* Fix *)
+
+TACTIC EXTEND fix
+  [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
+| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+END
+
+(* Cofix *)
+
+TACTIC EXTEND cofix
+  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
+| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+END
+
+(* Clear *)
+
+TACTIC EXTEND clear
+  [ "clear" hyp_list(ids) ] -> [
+    if List.is_empty ids then Tactics.keep []
+    else Proofview.V82.tactic (Tactics.clear ids)
+  ]
+| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
+END
+
+(* Clearbody *)
+
+TACTIC EXTEND clearbody
+  [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+END
+
+(* Generalize dependent *)
+
+TACTIC EXTEND generalize_dependent
+  [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
@@ -210,7 +279,6 @@ let initial_atomic () =
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
         "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
-        "cofix", TacCofix None;
       ]
   in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index cbb9db65c1..a069fd7557 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -491,11 +491,9 @@ let rec intern_atomic lf ist x =
       TacElim (ev,intern_constr_with_bindings_arg ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb)
-  | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
       TacMutualFix (intern_ident lf ist id, n, List.map f l)
-  | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
@@ -507,7 +505,6 @@ let rec intern_atomic lf ist x =
       TacGeneralize (List.map (fun (c,na) ->
 	               intern_constr_with_occurrences ist c,
                        intern_name lf ist na) cl)
-  | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
   | TacLetTac (na,c,cls,b,eqpat) ->
       let na = intern_name lf ist na in
       TacLetTac (na,intern_constr ist c,
@@ -527,18 +524,11 @@ let rec intern_atomic lf ist x =
       let h2 = intern_quantified_hypothesis ist h2 in
       TacDoubleInduction (h1,h2)
   (* Context management *)
-  | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l)
-  | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l)
-  | TacMove (id1,id2) ->
-    TacMove (intern_hyp ist id1,intern_move_location ist id2)
   | TacRename l ->
       TacRename (List.map (fun (id1,id2) ->
 			     intern_hyp ist id1,
 			     intern_hyp ist id2) l)
 
-  (* Constructors *)
-  | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
@@ -560,10 +550,6 @@ let rec intern_atomic lf ist x =
       TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
 	clause_app (intern_hyp_location ist) cl)
 
-  (* Equivalence relations *)
-  | TacSymmetry idopt ->
-      TacSymmetry (clause_app (intern_hyp_location ist) idopt)
-
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
       TacRewrite
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d5a1215b87..1a8a95158a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1749,15 +1749,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Tacticals.New.tclWITHHOLES ev named_tac sigma
       end }
-  | TacFix (idopt,n) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let idopt = Option.map (interp_ident ist env sigma) idopt in
-        name_atomic ~env
-          (TacFix(idopt,n))
-          (Proofview.V82.tactic (Tactics.fix idopt n))
-      end }
   | TacMutualFix (id,n,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
@@ -1773,15 +1764,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-  | TacCofix idopt ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let idopt = Option.map (interp_ident ist env sigma) idopt in
-        name_atomic ~env
-          (TacCofix (idopt))
-          (Proofview.V82.tactic (Tactics.cofix idopt))
-      end }
   | TacMutualCofix (id,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
@@ -1821,12 +1803,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (TacGeneralize cl)
           (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
       end }
-  | TacGeneralizeDep c ->
-      (new_interp_constr ist c) (fun c ->
-        name_atomic (* spiwack: probably needs a goal environment *)
-        (TacGeneralizeDep c)
-        (Proofview.V82.tactic (Tactics.generalize_dep c))
-       )
   | TacLetTac (na,c,clp,b,eqpat) ->
       Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -1899,31 +1875,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (TacDoubleInduction (h1,h2))
         (Elim.h_double_induction h1 h2)
   (* Context management *)
-  | TacClear (b,l) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l = interp_hyp_list ist env sigma l in
-        if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l)
-        else
-          (* spiwack: until the tactic is in the monad *)
-          let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in
-          Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac
-      end }
-  | TacClearBody l ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l = interp_hyp_list ist env sigma l in
-        name_atomic ~env
-          (TacClearBody l)
-          (Tactics.clear_body l)
-      end }
-  | TacMove (id1,id2) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1)
-                   (interp_move_location ist (pf_env gl) (project gl) id2))
-      end }
   | TacRename l ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = pf_env gl in
@@ -1938,18 +1889,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (Tactics.rename_hyp l)
       end }
 
-  (* Constructors *)
-  | TacSplit (ev,bll) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        let named_tac =
-          let tac = Tactics.split_with_bindings ev bll in
-          name_atomic ~env (TacSplit (ev, bll)) tac
-        in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma
-      end }
   (* Conversion *)
   | TacReduce (r,cl) ->
       (* spiwack: until the tactic is in the monad *)
@@ -2018,16 +1957,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end }
       end
 
-  (* Equivalence relations *)
-  | TacSymmetry c ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let cl = interp_clause ist env sigma c in
-        name_atomic ~env
-          (TacSymmetry cl)
-          (Tactics.intros_symmetry cl)
-      end }
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4a5fa9828e..3f103a290d 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -146,17 +146,14 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacElim (ev,subst_glob_with_bindings_arg subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)
   | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb)
-  | TacFix (idopt,n) as x -> x
   | TacMutualFix (id,n,l) ->
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
-  | TacCofix idopt as x -> x
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
   | TacAssert (b,otac,na,c) ->
       TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
-  | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
   | TacLetTac (id,c,clp,b,eqpat) ->
     TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
 
@@ -169,23 +166,14 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDoubleInduction (h1,h2) as x -> x
 
   (* Context management *)
-  | TacClear _ as x -> x
-  | TacClearBody l as x -> x
-  | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x
 
-  (* Constructors *)
-  | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)
-
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (op,c,cl) ->
       TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
         subst_glob_constr subst c, cl)
 
-  (* Equivalence relations *)
-  | TacSymmetry _ as x -> x
-
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
       TacRewrite (ev,