diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 8 |
3 files changed, 5 insertions, 8 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 19c09571f0..221c46a926 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -416,10 +416,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} let pp_info = ref (fun _ _ _ -> assert false) let set_info_printer f = pp_info := f -let tclINFO (tac : tactic) gls = - msgnl (hov 0 (str "Warning: info is currently not working")); - tac gls - (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma gl = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 75fd6d3d65..9d3d37c223 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -137,7 +137,6 @@ val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic -val tclINFO : tactic -> tactic (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, if it succeeds, applies [tac2] to the resulting subgoals, diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index a044f563f7..cec6fd4199 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -29,6 +29,8 @@ type split_flag = bool (* true = exists false = split *) type hidden_flag = bool (* true = internal use false = user-level *) type letin_flag = bool (* true = use local def false = use Leibniz *) +type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) + type glob_red_flag = | FBeta | FIota @@ -173,9 +175,9 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = | TacLApply of 'constr (* Automation tactics *) - | TacTrivial of 'constr list * string list option - | TacAuto of int or_var option * 'constr list * string list option - | TacDAuto of int or_var option * int option * 'constr list + | TacTrivial of debug * 'constr list * string list option + | TacAuto of debug * int or_var option * 'constr list * string list option + | TacDAuto of debug * int or_var option * int option * 'constr list (* Context management *) | TacClear of bool * 'id list |