Merging the e/- variants of primitive tactics.

3 files changed, 61 insertions, 95 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index ac530f5130..f63252ec22 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -163,41 +163,35 @@ let define_prim3 name tac =
   in
   Tac2env.define_primitive (pname name) tac
 
-(** Tactics from Tacexpr *)
+let define_prim4 name tac =
+  let tac = function
+  | [x; y; z; u] -> lift (tac x y z u)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
 
-let () = define_prim1 "tac_intros" begin fun ipat ->
-  let ipat = to_intro_patterns ipat in
-  Tactics.intros_patterns false ipat
-end
+(** Tactics from Tacexpr *)
 
-let () = define_prim1 "tac_eintros" begin fun ipat ->
+let () = define_prim2 "tac_intros" begin fun ev ipat ->
+  let ev = Value.to_bool ev in
   let ipat = to_intro_patterns ipat in
-  Tactics.intros_patterns true ipat
+  Tactics.intros_patterns ev ipat
 end
 
-let () = define_prim2 "tac_elim" begin fun c copt ->
+let () = define_prim3 "tac_elim" begin fun ev c copt ->
+  let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
   let copt = Value.to_option to_constr_with_bindings copt in
-  Tactics.elim false None c copt
+  Tactics.elim ev None c copt
 end
 
-let () = define_prim2 "tac_eelim" begin fun c copt ->
+let () = define_prim2 "tac_case" begin fun ev c ->
+  let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
-  let copt = Value.to_option to_constr_with_bindings copt in
-  Tactics.elim true None c copt
-end
-
-let () = define_prim1 "tac_case" begin fun c ->
-  let c = to_constr_with_bindings c in
-  Tactics.general_case_analysis false None c
+  Tactics.general_case_analysis ev None c
 end
 
-let () = define_prim1 "tac_ecase" begin fun c ->
-  let c = to_constr_with_bindings c in
-  Tactics.general_case_analysis true None c
-end
-
-let () = define_prim1 "tac_egeneralize" begin fun cl ->
+let () = define_prim1 "tac_generalize" begin fun cl ->
   let cast = function
   | ValBlk (0, [| c; occs; na |]) ->
     ((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
@@ -229,22 +223,14 @@ let () = define_prim2 "tac_pose" begin fun idopt c ->
   Tactics.letin_tac None na c None Locusops.nowhere
 end
 
-let () = define_prim3 "tac_set" begin fun idopt c cl ->
-  let na = to_name idopt in
-  let cl = to_clause cl in
-  Proofview.tclEVARMAP >>= fun sigma ->
-  thaw c >>= fun c ->
-  let c = Value.to_constr c in
-  Tactics.letin_pat_tac false None na (sigma, c) cl
-end
-
-let () = define_prim3 "tac_eset" begin fun idopt c cl ->
+let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
+  let ev = Value.to_bool ev in
   let na = to_name idopt in
   let cl = to_clause cl in
   Proofview.tclEVARMAP >>= fun sigma ->
   thaw c >>= fun c ->
   let c = Value.to_constr c in
-  Tactics.letin_pat_tac true None na (sigma, c) cl
+  Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
 let () = define_prim1 "tac_red" begin fun cl ->
@@ -301,21 +287,15 @@ let () = define_prim1 "tac_cut" begin fun c ->
   Tactics.cut c
 end
 
-let () = define_prim1 "tac_left" begin fun bnd ->
-  let bnd = to_bindings bnd in
-  Tactics.left_with_bindings false bnd
-end
-let () = define_prim1 "tac_eleft" begin fun bnd ->
+let () = define_prim2 "tac_left" begin fun ev bnd ->
+  let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
-  Tactics.left_with_bindings true bnd
+  Tactics.left_with_bindings ev bnd
 end
-let () = define_prim1 "tac_right" begin fun bnd ->
+let () = define_prim2 "tac_right" begin fun ev bnd ->
+  let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
-  Tactics.right_with_bindings false bnd
-end
-let () = define_prim1 "tac_eright" begin fun bnd ->
-  let bnd = to_bindings bnd in
-  Tactics.right_with_bindings true bnd
+  Tactics.right_with_bindings ev bnd
 end
 
 let () = define_prim1 "tac_introsuntil" begin fun h ->
@@ -334,19 +314,16 @@ let () = define_prim1 "tac_nativecastnocheck" begin fun c ->
   Tactics.native_cast_no_check (Value.to_constr c)
 end
 
-let () = define_prim0 "tac_constructor" (Tactics.any_constructor false None)
-let () = define_prim0 "tac_econstructor" (Tactics.any_constructor true None)
-
-let () = define_prim2 "tac_constructorn" begin fun n bnd ->
-  let n = Value.to_int n in
-  let bnd = to_bindings bnd in
-  Tactics.constructor_tac false None n bnd
+let () = define_prim1 "tac_constructor" begin fun ev ->
+  let ev = Value.to_bool ev in
+  Tactics.any_constructor ev None
 end
 
-let () = define_prim2 "tac_econstructorn" begin fun n bnd ->
+let () = define_prim3 "tac_constructorn" begin fun ev n bnd ->
+  let ev = Value.to_bool ev in
   let n = Value.to_int n in
   let bnd = to_bindings bnd in
-  Tactics.constructor_tac true None n bnd
+  Tactics.constructor_tac ev None n bnd
 end
 
 let () = define_prim1 "tac_symmetry" begin fun cl ->
@@ -354,14 +331,10 @@ let () = define_prim1 "tac_symmetry" begin fun cl ->
   Tactics.intros_symmetry cl
 end
 
-let () = define_prim1 "tac_split" begin fun bnd ->
-  let bnd = to_bindings bnd in
-  Tactics.split_with_bindings false [bnd]
-end
-
-let () = define_prim1 "tac_esplit" begin fun bnd ->
+let () = define_prim2 "tac_split" begin fun ev bnd ->
+  let ev = Value.to_bool ev in
   let bnd = to_bindings bnd in
-  Tactics.split_with_bindings true [bnd]
+  Tactics.split_with_bindings ev [bnd]
 end
 
 let () = define_prim1 "tac_rename" begin fun ids ->
diff --git a/theories/Notations.v b/theories/Notations.v
index ec7a6b0b12..0487e324ca 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -9,32 +9,32 @@
 Require Import Ltac2.Init.
 Require Ltac2.Control Ltac2.Std.
 
-Ltac2 Notation "intros" p(intropatterns) := Std.intros p.
+Ltac2 Notation "intros" p(intropatterns) := Std.intros false p.
 
-Ltac2 Notation "eintros" p(intropatterns) := Std.eintros p.
+Ltac2 Notation "eintros" p(intropatterns) := Std.intros true p.
 
 Ltac2 Notation "split" bnd(thunk(bindings)) :=
-  Control.with_holes bnd (fun bnd => Std.split bnd).
+  Control.with_holes bnd (fun bnd => Std.split false bnd).
 
-Ltac2 Notation "esplit" bnd(bindings) := Std.esplit bnd.
+Ltac2 Notation "esplit" bnd(bindings) := Std.split true bnd.
 
 Ltac2 Notation "left" bnd(thunk(bindings)) :=
-  Control.with_holes bnd (fun bnd => Std.left bnd).
+  Control.with_holes bnd (fun bnd => Std.left false bnd).
 
-Ltac2 Notation "eleft" bnd(bindings) := Std.eleft bnd.
+Ltac2 Notation "eleft" bnd(bindings) := Std.left true bnd.
 
 Ltac2 Notation "right" bnd(thunk(bindings)) :=
-  Control.with_holes bnd (fun bnd => Std.right bnd).
+  Control.with_holes bnd (fun bnd => Std.right false bnd).
 
-Ltac2 Notation "eright" bnd(bindings) := Std.eright bnd.
+Ltac2 Notation "eright" bnd(bindings) := Std.right true bnd.
 
-Ltac2 Notation "constructor" := Std.constructor ().
+Ltac2 Notation "constructor" := Std.constructor false.
 Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) :=
-  Control.with_holes bnd (fun bnd => Std.constructor_n n bnd).
+  Control.with_holes bnd (fun bnd => Std.constructor_n false n bnd).
 
-Ltac2 Notation "econstructor" := Std.econstructor ().
+Ltac2 Notation "econstructor" := Std.constructor true.
 Ltac2 Notation "econstructor" n(tactic) bnd(bindings) :=
-  Std.econstructor_n n bnd.
+  Std.constructor_n true n bnd.
 
 Ltac2 eelim c bnd use :=
     let use := match use with
@@ -42,7 +42,7 @@ Ltac2 eelim c bnd use :=
     | Some u =>
       let ((_, c, wth)) := u in Some (c, wth)
     end in
-  Std.eelim (c, bnd) use.
+  Std.elim true (c, bnd) use.
 
 Ltac2 elim c bnd use :=
   Control.with_holes
@@ -53,7 +53,7 @@ Ltac2 elim c bnd use :=
       | Some u =>
         let ((_, c, wth)) := u in Some (c, wth)
       end in
-    Std.elim (c, bnd) use).
+    Std.elim false (c, bnd) use).
 
 Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
   use(thunk(opt(seq("using", constr, bindings)))) := elim c bnd use.
diff --git a/theories/Std.v b/theories/Std.v
index 3d0f463c5e..20504f1247 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -73,24 +73,22 @@ with or_and_intro_pattern := [
 | IntroAndPattern (intro_pattern list)
 ].
 
+Ltac2 Type evar_flag := bool.
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
-Ltac2 @ external intros : intro_pattern list -> unit := "ltac2" "tac_intros".
-Ltac2 @ external eintros : intro_pattern list -> unit := "ltac2" "tac_eintros".
+Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "ltac2" "tac_intros".
 
-Ltac2 @ external elim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
-Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
-Ltac2 @ external case : constr_with_bindings -> unit := "ltac2" "tac_case".
-Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
+Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
+Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "tac_case".
 
-Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".
+Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_generalize".
 
 Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_assert".
 Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough".
 
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
-Ltac2 @ external set : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
-Ltac2 @ external eset : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_eset".
+Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
 
 Ltac2 @ external red : clause -> unit := "ltac2" "tac_red".
 Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf".
@@ -108,18 +106,13 @@ Ltac2 @ external etransitivity : unit -> unit := "ltac2" "tac_etransitivity".
 
 Ltac2 @ external cut : constr -> unit := "ltac2" "tac_cut".
 
-Ltac2 @ external left : bindings -> unit := "ltac2" "tac_left".
-Ltac2 @ external eleft : bindings -> unit := "ltac2" "tac_eleft".
-Ltac2 @ external right : bindings -> unit := "ltac2" "tac_right".
-Ltac2 @ external eright : bindings -> unit := "ltac2" "tac_eright".
+Ltac2 @ external left : evar_flag -> bindings -> unit := "ltac2" "tac_left".
+Ltac2 @ external right : evar_flag -> bindings -> unit := "ltac2" "tac_right".
 
-Ltac2 @ external constructor : unit -> unit := "ltac2" "tac_constructor".
-Ltac2 @ external econstructor : unit -> unit := "ltac2" "tac_econstructor".
-Ltac2 @ external split : bindings -> unit := "ltac2" "tac_split".
-Ltac2 @ external esplit : bindings -> unit := "ltac2" "tac_esplit".
+Ltac2 @ external constructor : evar_flag -> unit := "ltac2" "tac_constructor".
+Ltac2 @ external split : evar_flag -> bindings -> unit := "ltac2" "tac_split".
 
-Ltac2 @ external constructor_n : int -> bindings -> unit := "ltac2" "tac_constructorn".
-Ltac2 @ external econstructor_n : int -> bindings -> unit := "ltac2" "tac_econstructorn".
+Ltac2 @ external constructor_n : evar_flag -> int -> bindings -> unit := "ltac2" "tac_constructorn".
 
 Ltac2 @ external intros_until : hypothesis -> unit := "ltac2" "tac_introsuntil".