Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 0 insertions, 366 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
deleted file mode 100644
index 931633e1..00000000
--- a/plugins/ltac/coretactics.ml4
+++ /dev/null
@@ -1,366 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Locus
-open Misctypes
-open Genredexpr
-open Stdarg
-open Extraargs
-open Names
-
-DECLARE PLUGIN "ltac_plugin"
-
-(** Basic tactics *)
-
-TACTIC EXTEND reflexivity
-  [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
-END
-
-TACTIC EXTEND exact
-  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
-END
-
-TACTIC EXTEND assumption
-  [ "assumption" ] -> [ Tactics.assumption ]
-END
-
-TACTIC EXTEND etransitivity
-  [ "etransitivity" ] -> [ Tactics.intros_transitivity None ]
-END
-
-TACTIC EXTEND cut
-  [ "cut" constr(c) ] -> [ Tactics.cut c ]
-END
-
-TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
-END
-
-TACTIC EXTEND vm_cast_no_check
-  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
-END
-
-TACTIC EXTEND native_cast_no_check
-  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
-END
-
-TACTIC EXTEND casetype
-  [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
-END
-
-TACTIC EXTEND elimtype
-  [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
-END
-
-TACTIC EXTEND lapply
-  [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
-END
-
-TACTIC EXTEND transitivity
-  [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
-END
-
-(** Left *)
-
-TACTIC EXTEND left
-  [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ]
-END
-
-TACTIC EXTEND eleft
-  [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ]
-END
-
-TACTIC EXTEND left_with
-  [ "left" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
-  ]
-END
-
-TACTIC EXTEND eleft_with
-  [ "eleft" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
-  ]
-END
-
-(** Right *)
-
-TACTIC EXTEND right
-  [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ]
-END
-
-TACTIC EXTEND eright
-  [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ]
-END
-
-TACTIC EXTEND right_with
-  [ "right" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
-  ]
-END
-
-TACTIC EXTEND eright_with
-  [ "eright" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
-  ]
-END
-
-(** Constructor *)
-
-TACTIC EXTEND constructor
-  [ "constructor" ] -> [ Tactics.any_constructor false None ]
-| [ "constructor" int_or_var(i) ] -> [
-    Tactics.constructor_tac false None i NoBindings
-  ]
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
-    let tac bl = Tactics.constructor_tac false None i bl in
-    Tacticals.New.tclDELAYEDWITHHOLES false bl tac
-  ]
-END
-
-TACTIC EXTEND econstructor
-  [ "econstructor" ] -> [ Tactics.any_constructor true None ]
-| [ "econstructor" int_or_var(i) ] -> [
-    Tactics.constructor_tac true None i NoBindings
-  ]
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
-    let tac bl = Tactics.constructor_tac true None i bl in
-    Tacticals.New.tclDELAYEDWITHHOLES true bl tac
-  ]
-END
-
-(** Specialize *)
-
-TACTIC EXTEND specialize
-  [ "specialize" constr_with_bindings(c) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
-  ]
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
-  ]
-END
-
-TACTIC EXTEND symmetry
-  [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-END
-
-TACTIC EXTEND symmetry_in
-| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
-END
-
-(** Split *)
-
-let rec delayed_list = function
-| [] -> fun _ sigma -> (sigma, [])
-| x :: l ->
-  fun env sigma ->
-    let (sigma, x) = x env sigma in
-    let (sigma, l) = delayed_list l env sigma in
-    (sigma, x :: l)
-
-TACTIC EXTEND split
-  [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
-END
-
-TACTIC EXTEND esplit
-  [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
-END
-
-TACTIC EXTEND split_with
-  [ "split" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
-  ]
-END
-
-TACTIC EXTEND esplit_with
-  [ "esplit" "with" bindings(bl) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
-  ]
-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
-
-TACTIC EXTEND intro
-| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
-| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
-| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
-| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
-| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
-| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
-END
-
-(** Move *)
-
-TACTIC EXTEND move
-  [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
-END
-
-(** Rename *)
-
-TACTIC EXTEND rename
-| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
-END
-
-(** Revert *)
-
-TACTIC EXTEND revert
-  [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
-END
-
-(** Simple induction / destruct *)
-
-let simple_induct h =
-  Tacticals.New.tclTHEN (Tactics.intros_until h)
-    (Tacticals.New.onLastHyp Tactics.simplest_elim)
-
-TACTIC EXTEND simple_induction
-  [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ]
-END
-
-let simple_destruct h =
-  Tacticals.New.tclTHEN (Tactics.intros_until h)
-    (Tacticals.New.onLastHyp Tactics.simplest_case)
-
-TACTIC EXTEND simple_destruct
-  [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ]
-END
-
-(** Double induction *)
-
-TACTIC EXTEND double_induction
-  [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
-  [ Elim.h_double_induction h1 h2 ]
-END
-
-(* Admit *)
-
-TACTIC EXTEND admit
- [ "admit" ] -> [ Proofview.give_up ]
-END
-
-(* Fix *)
-
-TACTIC EXTEND fix
-  [ "fix" natural(n) ] -> [ Tactics.fix None n ]
-| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
-END
-
-(* Cofix *)
-
-TACTIC EXTEND cofix
-  [ "cofix" ] -> [ Tactics.cofix None ]
-| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
-END
-
-(* Clear *)
-
-TACTIC EXTEND clear
-  [ "clear" hyp_list(ids) ] -> [
-    if List.is_empty ids then Tactics.keep []
-    else 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) ] -> [ Tactics.generalize_dep c ]
-END
-
-(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
-
-open Tacexpr
-
-let initial_atomic () =
-  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
-  let iter (s, t) =
-    let body = TacAtom (Loc.tag t) in
-    Tacenv.register_ltac false false (Names.Id.of_string s) body
-  in
-  let () = List.iter iter
-      [ "red", TacReduce(Red false,nocl);
-        "hnf", TacReduce(Hnf,nocl);
-        "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl);
-        "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intros", TacIntroPattern (false,[]);
-      ]
-  in
-  let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in
-  List.iter iter
-      [ "idtac",TacId [];
-        "fail", TacFail(TacLocal,ArgArg 0,[]);
-        "fresh", TacArg(Loc.tag @@ TacFreshId [])
-      ]
-
-let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
-
-(* First-class Ltac access to primitive blocks *)
-
-let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
-let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
-
-let register_list_tactical name f =
-  let tac args ist = match args with
-  | [v] ->
-    begin match Tacinterp.Value.to_list v with
-    | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list")
-    | Some tacs ->
-      let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in
-      f tacs
-    end
-  | _ -> assert false
-  in
-  Tacenv.register_ml_tactic (initial_name name) [|tac|]
-
-let () = register_list_tactical "first" Tacticals.New.tclFIRST
-let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
-
-let initial_tacticals () =
-  let idn n = Id.of_string (Printf.sprintf "_%i" n) in
-  let varn n = Reference (ArgVar (CAst.make (idn n))) in
-  let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
-  List.iter iter [
-    "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
-    "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
-  ]
-
-let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"