diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/coretactics.ml4 | 34 | ||||
-rw-r--r-- | tactics/tacenv.ml | 44 | ||||
-rw-r--r-- | tactics/tacenv.mli | 8 | ||||
-rw-r--r-- | tactics/tacintern.ml | 7 | ||||
-rw-r--r-- | tactics/tacintern.mli | 1 |
5 files changed, 36 insertions, 58 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index cbac5c73a..d429dc07e 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -9,8 +9,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Util +open Names open Locus open Misctypes +open Genredexpr open Proofview.Notations @@ -187,3 +189,35 @@ END TACTIC EXTEND simple_destruct [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] END + +(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) + +open Tacexpr + +let initial_atomic () = + let dloc = Loc.ghost in + let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in + let iter (s, t) = + let body = TacAtom (dloc, t) in + Tacenv.register_ltac false (Id.of_string s) body + in + let ans = List.iter iter + [ "red", TacReduce(Red false,nocl); + "hnf", TacReduce(Hnf,nocl); + "simpl", TacReduce(Simpl None,nocl); + "compute", TacReduce(Cbv Redops.all_flags,nocl); + "intro", TacIntroMove(None,MoveLast); + "intros", TacIntroPattern []; + "cofix", TacCofix None; + "trivial", TacTrivial (Off,[],None); + "auto", TacAuto(Off,None,[],None); + ] + in + let iter (s, t) = Tacenv.register_ltac false (Id.of_string s) t in + List.iter iter + [ "idtac",TacId []; + "fail", TacFail(ArgArg 0,[]); + "fresh", TacArg(dloc,TacFreshId []) + ] + +let () = Mltop.declare_cache_obj initial_atomic "coretactics" diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9bef0d3bb..8f9cd8662 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -69,47 +69,6 @@ let () = let assert_installed opn = let _ = interp_ml_tactic opn in () in Hook.set Tacintern.assert_tactic_installed_hook assert_installed -(** Coq tactic definitions. *) - -(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) - - -let initial_atomic = - let open Locus in - let open Misctypes in - let open Genredexpr in - let dloc = Loc.ghost in - let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in - let fold accu (s, t) = - let body = TacAtom (dloc, t) in - Id.Map.add (Id.of_string s) body accu - in - let ans = List.fold_left fold Id.Map.empty - [ "red", TacReduce(Red false,nocl); - "hnf", TacReduce(Hnf,nocl); - "simpl", TacReduce(Simpl None,nocl); - "compute", TacReduce(Cbv Redops.all_flags,nocl); - "intro", TacIntroMove(None,MoveLast); - "intros", TacIntroPattern []; - "cofix", TacCofix None; - "trivial", TacTrivial (Off,[],None); - "auto", TacAuto(Off,None,[],None); - ] - in - let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in - List.fold_left fold ans - [ "idtac",TacId []; - "fail", TacFail(ArgArg 0,[]); - "fresh", TacArg(dloc,TacFreshId []) - ] - -let atomic_mactab = Summary.ref ~name:"atomic_tactics" initial_atomic - -let register_atomic_ltac id tac = - atomic_mactab := Id.Map.add id tac !atomic_mactab - -let interp_atomic_ltac id = Id.Map.find id !atomic_mactab - (***************************************************************************) (* Tactic registration *) @@ -186,5 +145,4 @@ let redefine_ltac local kn tac = Lib.add_anonymous_leaf (inMD (local, (UpdateTac kn, tac))) let () = - Hook.set Tacintern.interp_ltac_hook interp_ltac; - Hook.set Tacintern.interp_atomic_ltac_hook interp_atomic_ltac + Hook.set Tacintern.interp_ltac_hook interp_ltac diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 3bc8040d7..841e1b390 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -25,14 +25,6 @@ val interp_alias : alias -> glob_tactic_expr (** {5 Coq tactic definitions} *) -(** FIXME: one day we should merge atomic tactics and user-defined ones. *) - -val register_atomic_ltac : Id.t -> glob_tactic_expr -> unit -(** Register a Coq built-in tactic. Should not be used by plugins. *) - -val interp_atomic_ltac : Id.t -> glob_tactic_expr -(** Find a Coq built-in tactic by name. Raise [Not_found] if it is absent. *) - val register_ltac : bool -> Id.t -> glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. If the boolean flag is set to true, then this is a local definition. It also puts the Ltac name in the diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index eea3cd98c..d4b6ef292 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -146,18 +146,13 @@ let intern_move_location ist = function | MoveFirst -> MoveFirst | MoveLast -> MoveLast -let (f_interp_atomic_ltac, interp_atomic_ltac_hook) = Hook.make () let (f_interp_ltac, interp_ltac_hook) = Hook.make () (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - try TacCall (loc,ArgArg (loc,locate_tactic qid),[]) - with Not_found -> - match r with - | Ident (_, id) -> Tacexp (Hook.get f_interp_atomic_ltac id) - | _ -> raise Not_found + TacCall (loc,ArgArg (loc,locate_tactic qid),[]) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 84e5782f8..2f6eb60f4 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -64,6 +64,5 @@ val dump_glob_red_expr : raw_red_expr -> unit (* Hooks *) val assert_tactic_installed_hook : (ml_tactic_name -> unit) Hook.t -val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t val strict_check : bool ref |