Making Ltac2 representation of data coincide with the ML-side one.

3 files changed, 252 insertions, 62 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e94027c899..07b01b1174 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -13,6 +13,7 @@ open Misctypes
 open Genredexpr
 open Tac2expr
 open Tac2ffi
+open Tac2tactics
 open Proofview.Notations
 
 module Value = Tac2ffi
@@ -39,7 +40,7 @@ let to_bindings = function
 | ValBlk (0, [| vl |]) ->
   ImplicitBindings (Value.to_list Value.to_constr vl)
 | ValBlk (1, [| vl |]) ->
-  ExplicitBindings ((Value.to_list (fun p -> None, to_pair to_qhyp Value.to_constr p) vl))
+  ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
 | _ -> assert false
 
 let to_constr_with_bindings = function
@@ -89,8 +90,7 @@ let to_pattern_with_occs pat =
   to_pair Value.to_pattern (fun occ -> to_occurrences to_int_or_var occ) pat
 
 let to_constr_with_occs c =
-  let (c, occ) = to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c in
-  (occ, c)
+  to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c
 
 let rec to_intro_pattern = function
 | ValBlk (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
@@ -108,9 +108,11 @@ and to_intro_pattern_action = function
 | ValInt 0 -> IntroWildcard
 | ValBlk (0, [| op |]) -> IntroOrAndPattern (to_or_and_intro_pattern op)
 | ValBlk (1, [| inj |]) ->
-  let map ipat = Loc.tag (to_intro_pattern ipat) in
+  let map ipat = to_intro_pattern ipat in
   IntroInjection (Value.to_list map inj)
-| ValBlk (2, [| _ |]) -> IntroApplyOn (assert false, assert false) (** TODO *)
+| ValBlk (2, [| c; ipat |]) ->
+  let c = thaw c >>= fun c -> return (Value.to_constr c) in
+  IntroApplyOn (c, to_intro_pattern ipat)
 | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
 | _ -> assert false
 
@@ -122,22 +124,21 @@ and to_or_and_intro_pattern = function
 | _ -> assert false
 
 and to_intro_patterns il =
-  let map ipat = Loc.tag (to_intro_pattern ipat) in
-  Value.to_list map il
+  Value.to_list to_intro_pattern il
 
 let to_destruction_arg = function
 | ValBlk (0, [| c |]) ->
   let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
-  None, ElimOnConstr c
-| ValBlk (1, [| id |]) -> None, ElimOnIdent (Loc.tag (Value.to_ident id))
-| ValBlk (2, [| n |]) -> None, ElimOnAnonHyp (Value.to_int n)
+  ElimOnConstr c
+| ValBlk (1, [| id |]) -> ElimOnIdent (Value.to_ident id)
+| ValBlk (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
 | _ -> assert false
 
 let to_induction_clause = function
 | ValBlk (0, [| arg; eqn; as_; in_ |]) ->
   let arg = to_destruction_arg arg in
-  let eqn = Value.to_option (fun p -> Loc.tag (to_intro_pattern_naming p)) eqn in
-  let as_ = Value.to_option (fun p -> Loc.tag (to_or_and_intro_pattern p)) as_ in
+  let eqn = Value.to_option to_intro_pattern_naming eqn in
+  let as_ = Value.to_option to_or_and_intro_pattern as_ in
   let in_ = Value.to_option to_clause in_ in
   (arg, eqn, as_, in_)
 | _ ->
@@ -218,7 +219,7 @@ let define_prim5 name tac =
 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 ev ipat
+  Tac2tactics.intros_patterns ev ipat
 end
 
 let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
@@ -226,7 +227,7 @@ let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
   let ev = Value.to_bool ev in
   let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
   let cb = Value.to_list map_cb cb in
-  let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in
+  let map p = Value.to_option to_intro_pattern p in
   let map_ipat p = to_pair Value.to_ident map p in
   let ipat = Value.to_option map_ipat ipat in
   Tac2tactics.apply adv ev cb ipat
@@ -236,13 +237,13 @@ 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 ev None c copt
+  Tac2tactics.elim ev c copt
 end
 
 let () = define_prim2 "tac_case" begin fun ev c ->
   let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
-  Tactics.general_case_analysis ev None c
+  Tac2tactics.general_case_analysis ev c
 end
 
 let () = define_prim1 "tac_generalize" begin fun cl ->
@@ -259,16 +260,16 @@ let () = define_prim3 "tac_assert" begin fun c tac ipat ->
   let c = Value.to_constr c in
   let of_tac t = Proofview.tclIGNORE (thaw t) in
   let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
-  let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
-  Tactics.forward true tac ipat c
+  let ipat = Value.to_option to_intro_pattern ipat in
+  Tac2tactics.forward true tac ipat c
 end
 
 let () = define_prim3 "tac_enough" begin fun c tac ipat ->
   let c = Value.to_constr c in
   let of_tac t = Proofview.tclIGNORE (thaw t) in
   let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
-  let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
-  Tactics.forward false tac ipat c
+  let ipat = Value.to_option to_intro_pattern ipat in
+  Tac2tactics.forward false tac ipat c
 end
 
 let () = define_prim2 "tac_pose" begin fun idopt c ->
@@ -297,7 +298,7 @@ let () = define_prim5 "tac_remember" begin fun ev na c eqpat cl ->
     Proofview.tclEVARMAP >>= fun sigma ->
     thaw c >>= fun c ->
     let c = Value.to_constr c in
-    Tactics.letin_pat_tac ev (Some (true, Loc.tag eqpat)) na (sigma, c) cl
+    Tac2tactics.letin_pat_tac ev (Some (true, eqpat)) na (sigma, c) cl
   | _ ->
     Tacticals.New.tclZEROMSG (Pp.str "Invalid pattern for remember")
 end
@@ -367,7 +368,7 @@ end
 let () = define_prim2 "tac_pattern" begin fun where cl ->
   let where = Value.to_list to_constr_with_occs where in
   let cl = to_clause cl in
-  Tactics.reduce (Pattern where) cl
+  Tac2tactics.pattern where cl
 end
 
 let () = define_prim2 "tac_vm" begin fun where cl ->
@@ -476,7 +477,7 @@ end
 let () = define_prim4 "tac_inversion" begin fun knd arg pat ids ->
   let knd = to_inversion_kind knd in
   let arg = to_destruction_arg arg in
-  let pat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) pat in
+  let pat = Value.to_option to_intro_pattern pat in
   let ids = Value.to_option (fun l -> Value.to_list Value.to_ident l) ids in
   Tac2tactics.inversion knd arg pat ids
 end
@@ -523,12 +524,12 @@ end
 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 ev bnd
+  Tac2tactics.left_with_bindings ev bnd
 end
 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 ev bnd
+  Tac2tactics.right_with_bindings ev bnd
 end
 
 let () = define_prim1 "tac_introsuntil" begin fun h ->
@@ -556,7 +557,7 @@ 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 ev None n bnd
+  Tac2tactics.constructor_tac ev None n bnd
 end
 
 let () = define_prim1 "tac_symmetry" begin fun cl ->
@@ -567,7 +568,7 @@ end
 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 ev [bnd]
+  Tac2tactics.split_with_bindings ev bnd
 end
 
 let () = define_prim1 "tac_rename" begin fun ids ->
@@ -633,7 +634,7 @@ end
 
 let () = define_prim1 "tac_contradiction" begin fun c ->
   let c = Value.to_option to_constr_with_bindings c in
-  Contradiction.contradiction c
+  Tac2tactics.contradiction c
 end
 
 let () = define_prim4 "tac_autorewrite" begin fun all by ids cl ->
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index aa2ee4711a..083ec9e9d4 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -16,7 +16,41 @@ open Genredexpr
 open Proofview
 open Proofview.Notations
 
-type destruction_arg = EConstr.constr with_bindings tactic Misctypes.destruction_arg
+let return = Proofview.tclUNIT
+
+type explicit_bindings = (quantified_hypothesis * EConstr.t) list
+
+type bindings =
+| ImplicitBindings of EConstr.t list
+| ExplicitBindings of explicit_bindings
+| NoBindings
+
+type constr_with_bindings = EConstr.constr * bindings
+
+type intro_pattern =
+| IntroForthcoming of bool
+| IntroNaming of intro_pattern_naming
+| IntroAction of intro_pattern_action
+and intro_pattern_naming =
+| IntroIdentifier of Id.t
+| IntroFresh of Id.t
+| IntroAnonymous
+and intro_pattern_action =
+| IntroWildcard
+| IntroOrAndPattern of or_and_intro_pattern
+| IntroInjection of intro_pattern list
+| IntroApplyOn of EConstr.t tactic * intro_pattern
+| IntroRewrite of bool
+and or_and_intro_pattern =
+| IntroOrPattern of intro_pattern list list
+| IntroAndPattern of intro_pattern list
+
+type core_destruction_arg =
+| ElimOnConstr of constr_with_bindings tactic
+| ElimOnIdent of Id.t
+| ElimOnAnonHyp of int
+
+type destruction_arg = core_destruction_arg
 
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
@@ -31,12 +65,57 @@ let delayed_of_tactic tac env sigma =
   let c, pv, _, _ = Proofview.apply env tac pv in
   (sigma, c)
 
+let mk_bindings = function
+| ImplicitBindings l -> Misctypes.ImplicitBindings l
+| ExplicitBindings l ->
+  let l = List.map Loc.tag l in
+  Misctypes.ExplicitBindings l
+| NoBindings -> Misctypes.NoBindings
+
+let mk_with_bindings (x, b) = (x, mk_bindings b)
+
+let rec mk_intro_pattern = function
+| IntroForthcoming b -> Loc.tag @@ Misctypes.IntroForthcoming b
+| IntroNaming ipat -> Loc.tag @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
+| IntroAction ipat -> Loc.tag @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)
+
+and mk_intro_pattern_naming = function
+| IntroIdentifier id -> Misctypes.IntroIdentifier id
+| IntroFresh id -> Misctypes.IntroFresh id
+| IntroAnonymous -> Misctypes.IntroAnonymous
+
+and mk_intro_pattern_action = function
+| IntroWildcard -> Misctypes.IntroWildcard
+| IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
+| IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
+| IntroApplyOn (c, ipat) ->
+  let c = Loc.tag @@ delayed_of_tactic c in
+  Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
+| IntroRewrite b -> Misctypes.IntroRewrite b
+
+and mk_or_and_intro_pattern = function
+| IntroOrPattern ipatss ->
+  Misctypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
+| IntroAndPattern ipats ->
+  Misctypes.IntroAndPattern (List.map mk_intro_pattern ipats)
+
+let mk_intro_patterns ipat = List.map mk_intro_pattern ipat
+
+let intros_patterns ev ipat =
+  let ipat = mk_intro_patterns ipat in
+  Tactics.intro_patterns ev ipat
+
 let apply adv ev cb cl =
-  let map c = None, Loc.tag (delayed_of_tactic c) in
+  let map c =
+    let c = c >>= fun c -> return (mk_with_bindings c) in
+    None, Loc.tag (delayed_of_tactic c)
+  in
   let cb = List.map map cb in
   match cl with
   | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
-  | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
+  | Some (id, cl) ->
+    let cl = Option.map mk_intro_pattern cl in
+    Tactics.apply_delayed_in adv ev id cb cl
 
 type induction_clause =
   destruction_arg *
@@ -44,31 +123,70 @@ type induction_clause =
   or_and_intro_pattern option *
   Locus.clause option
 
-let map_destruction_arg = function
-| ElimOnConstr c -> ElimOnConstr (delayed_of_tactic c)
-| ElimOnIdent id -> ElimOnIdent id
-| ElimOnAnonHyp n -> ElimOnAnonHyp n
+let mk_destruction_arg = function
+| ElimOnConstr c ->
+  let c = c >>= fun c -> return (mk_with_bindings c) in
+  Misctypes.ElimOnConstr (delayed_of_tactic c)
+| ElimOnIdent id -> Misctypes.ElimOnIdent (Loc.tag id)
+| ElimOnAnonHyp n -> Misctypes.ElimOnAnonHyp n
+
+let mk_induction_clause (arg, eqn, as_, occ) =
+  let eqn = Option.map (fun ipat -> Loc.tag @@ mk_intro_pattern_naming ipat) eqn in
+  let as_ = Option.map (fun ipat -> Loc.tag @@ mk_or_and_intro_pattern ipat) as_ in
+  ((None, mk_destruction_arg arg), (eqn, as_), occ)
+
+let induction_destruct isrec ev (ic : induction_clause list) using =
+  let ic = List.map mk_induction_clause ic in
+  let using = Option.map mk_with_bindings using in
+  Tactics.induction_destruct isrec ev (ic, using)
+
+let elim ev c copt =
+  let c = mk_with_bindings c in
+  let copt = Option.map mk_with_bindings copt in
+  Tactics.elim ev None c copt
 
-let map_induction_clause ((clear, arg), eqn, as_, occ) =
-  ((clear, map_destruction_arg arg), (eqn, as_), occ)
+let general_case_analysis ev c =
+  let c = mk_with_bindings c in
+  Tactics.general_case_analysis ev None c
 
-let induction_destruct isrec ev ic using =
-  let ic = List.map map_induction_clause ic in
-  Tactics.induction_destruct isrec ev (ic, using)
+let constructor_tac ev n i bnd =
+  let bnd = mk_bindings bnd in
+  Tactics.constructor_tac ev n i bnd
+
+let left_with_bindings ev bnd =
+  let bnd = mk_bindings bnd in
+  Tactics.left_with_bindings ev bnd
+
+let right_with_bindings ev bnd =
+  let bnd = mk_bindings bnd in
+  Tactics.right_with_bindings ev bnd
+
+let split_with_bindings ev bnd =
+  let bnd = mk_bindings bnd in
+  Tactics.split_with_bindings ev [bnd]
 
 type rewriting =
   bool option *
   multi *
-  EConstr.constr with_bindings tactic
+  constr_with_bindings tactic
 
 let rewrite ev rw cl by =
   let map_rw (orient, repeat, c) =
+    let c = c >>= fun c -> return (mk_with_bindings c) in
     (Option.default true orient, repeat, None, delayed_of_tactic c)
   in
   let rw = List.map map_rw rw in
   let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
   Equality.general_multi_rewrite ev rw cl by
 
+let forward ev tac ipat c =
+  let ipat = Option.map mk_intro_pattern ipat in
+  Tactics.forward ev tac ipat c
+
+let letin_pat_tac ev ipat na c cl =
+  let ipat = Option.map (fun (b, ipat) -> (b, Loc.tag @@ mk_intro_pattern_naming ipat)) ipat in
+  Tactics.letin_pat_tac ev ipat na c cl
+
 (** Ltac interface treats differently global references than other term
     arguments in reduction expressions. In Ltac1, this is done at parsing time.
     Instead, we parse indifferently any pattern and dispatch when the tactic is
@@ -114,6 +232,10 @@ let unfold occs cl =
   Proofview.Monad.List.map map occs >>= fun occs ->
   Tactics.reduce (Unfold occs) cl
 
+let pattern where cl =
+  let where = List.map (fun (c, occ) -> (occ, c)) where in
+  Tactics.reduce (Pattern where) cl
+
 let vm where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvVm where) cl
@@ -189,12 +311,13 @@ let on_destruction_arg tac ev arg =
       let env = Proofview.Goal.env gl in
       Proofview.tclEVARMAP >>= fun sigma ->
       c >>= fun (c, lbind) ->
+      let lbind = mk_bindings lbind in
       Proofview.tclEVARMAP >>= fun sigma' ->
       let flags = tactic_infer_flags ev in
       let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in
-      Proofview.tclUNIT (Some sigma', ElimOnConstr (c, lbind))
-    | ElimOnIdent id -> Proofview.tclUNIT (None, ElimOnIdent id)
-    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, ElimOnAnonHyp n)
+      Proofview.tclUNIT (Some sigma', Misctypes.ElimOnConstr (c, lbind))
+    | ElimOnIdent id -> Proofview.tclUNIT (None, Misctypes.ElimOnIdent (Loc.tag id))
+    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Misctypes.ElimOnAnonHyp n)
     in
     arg >>= fun (sigma', arg) ->
     let arg = Some (clear, arg) in
@@ -204,9 +327,13 @@ let on_destruction_arg tac ev arg =
       Tacticals.New.tclWITHHOLES ev (tac ev arg) sigma'
   end
 
-let discriminate ev arg = on_destruction_arg Equality.discr_tac ev arg
+let discriminate ev arg =
+  let arg = Option.map (fun arg -> None, arg) arg in
+  on_destruction_arg Equality.discr_tac ev arg
 
 let injection ev ipat arg =
+  let arg = Option.map (fun arg -> None, arg) arg in
+  let ipat = Option.map mk_intro_patterns ipat in
   let tac ev arg = Equality.injClause ipat ev arg in
   on_destruction_arg tac ev arg
 
@@ -262,25 +389,30 @@ let inversion knd arg pat ids =
   in
   begin match pat with
   | None -> Proofview.tclUNIT None
-  | Some (_, IntroAction (IntroOrAndPattern p)) ->
-    Proofview.tclUNIT (Some (Loc.tag p))
+  | Some (IntroAction (IntroOrAndPattern p)) ->
+    Proofview.tclUNIT (Some (Loc.tag @@ mk_or_and_intro_pattern p))
   | Some _ ->
     Tacticals.New.tclZEROMSG (str "Inversion only accept disjunctive patterns")
   end >>= fun pat ->
   let inversion _ arg =
     begin match arg with
     | None -> assert false
-    | Some (_, ElimOnAnonHyp n) ->
+    | Some (_, Misctypes.ElimOnAnonHyp n) ->
       Inv.inv_clause knd pat ids (AnonHyp n)
-    | Some (_, ElimOnIdent (_, id)) ->
+    | Some (_, Misctypes.ElimOnIdent (_, id)) ->
       Inv.inv_clause knd pat ids (NamedHyp id)
-    | Some (_, ElimOnConstr c) ->
+    | Some (_, Misctypes.ElimOnConstr c) ->
+      let open Misctypes in
       let anon = Loc.tag @@ IntroNaming IntroAnonymous in
       Tactics.specialize c (Some anon) >>= fun () ->
       Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
     end
   in
-  on_destruction_arg inversion true (Some arg)
+  on_destruction_arg inversion true (Some (None, arg))
+
+let contradiction c =
+  let c = Option.map mk_with_bindings c in
+  Contradiction.contradiction c
 
 (** Firstorder *)
 
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index f6825d84aa..5fdd1c39bc 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -16,13 +16,41 @@ open Misctypes
 open Tactypes
 open Proofview
 
-type destruction_arg = EConstr.constr with_bindings tactic Misctypes.destruction_arg
-
-(** Local reimplementations of tactics variants from Coq *)
-
-val apply : advanced_flag -> evars_flag ->
-  EConstr.constr with_bindings tactic list ->
-  (Id.t * intro_pattern option) option -> unit tactic
+(** Redefinition of Ltac1 data structures because of impedance mismatch *)
+
+type explicit_bindings = (quantified_hypothesis * EConstr.t) list
+
+type bindings =
+| ImplicitBindings of EConstr.t list
+| ExplicitBindings of explicit_bindings
+| NoBindings
+
+type constr_with_bindings = EConstr.constr * bindings
+
+type core_destruction_arg =
+| ElimOnConstr of constr_with_bindings tactic
+| ElimOnIdent of Id.t
+| ElimOnAnonHyp of int
+
+type destruction_arg = core_destruction_arg
+
+type intro_pattern =
+| IntroForthcoming of bool
+| IntroNaming of intro_pattern_naming
+| IntroAction of intro_pattern_action
+and intro_pattern_naming =
+| IntroIdentifier of Id.t
+| IntroFresh of Id.t
+| IntroAnonymous
+and intro_pattern_action =
+| IntroWildcard
+| IntroOrAndPattern of or_and_intro_pattern
+| IntroInjection of intro_pattern list
+| IntroApplyOn of EConstr.t tactic * intro_pattern
+| IntroRewrite of bool
+and or_and_intro_pattern =
+| IntroOrPattern of intro_pattern list list
+| IntroAndPattern of intro_pattern list
 
 type induction_clause =
   destruction_arg *
@@ -30,17 +58,42 @@ type induction_clause =
   or_and_intro_pattern option *
   clause option
 
-val induction_destruct : rec_flag -> evars_flag ->
-  induction_clause list -> EConstr.constr with_bindings option -> unit tactic
-
 type rewriting =
   bool option *
   multi *
-  EConstr.constr with_bindings tactic
+  constr_with_bindings tactic
+
+(** Local reimplementations of tactics variants from Coq *)
+
+val intros_patterns : evars_flag -> intro_pattern list -> unit tactic
+
+val apply : advanced_flag -> evars_flag ->
+  constr_with_bindings tactic list ->
+  (Id.t * intro_pattern option) option -> unit tactic
+
+val induction_destruct : rec_flag -> evars_flag ->
+  induction_clause list -> constr_with_bindings option -> unit tactic
+
+val elim : evars_flag -> constr_with_bindings -> constr_with_bindings option ->
+  unit tactic
+
+val general_case_analysis : evars_flag -> constr_with_bindings ->  unit tactic
+
+val constructor_tac : evars_flag -> int option -> int -> bindings -> unit tactic
+
+val left_with_bindings  : evars_flag -> bindings -> unit tactic
+val right_with_bindings : evars_flag -> bindings -> unit tactic
+val split_with_bindings : evars_flag -> bindings -> unit tactic
 
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
 
+val forward : bool -> unit tactic option option ->
+  intro_pattern option -> constr -> unit tactic
+
+val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
+  Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic
+
 val simpl : global_reference glob_red_flag ->
   (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
@@ -52,6 +105,8 @@ val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
 
 val unfold : (global_reference * occurrences_expr) list -> clause -> unit tactic
 
+val pattern : (constr * occurrences_expr) list -> clause -> unit tactic
+
 val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
 val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
@@ -102,4 +157,6 @@ val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
 
 val inversion : inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
+val contradiction : constr_with_bindings option -> unit tactic
+
 val firstorder : unit Proofview.tactic option -> global_reference list -> Id.t list -> unit tactic