From ebf4d8e58eeddaf5237447a9a0f21de48e72caa5 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 19 Feb 2015 11:23:03 +0100 Subject: [info] tactical warning: do not suggest [info_auto] and [info_trivial]. Since they don't work anymore. --- tactics/tacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3b497faab5..e4558481bc 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with msg_warning (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ strbrk "There is an \"Info\" command to replace it." ++fnl () ++ - strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto."); + strbrk "Some specific verbose tactics may also exist, such as info_eauto."); eval_tactic ist tac (* For extensions *) | TacAlias (loc,s,l) -> -- cgit v1.2.3 From 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 19 Feb 2015 11:28:19 +0100 Subject: [info_auto] & [info_trivial]: warning message to help users find [Info]. --- tactics/tacinterp.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'tactics') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e4558481bc..af541b8b9e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1973,6 +1973,12 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Automation tactics *) | TacTrivial (debug,lems,l) -> + begin if debug == Tacexpr.Info then + msg_warning + (strbrk"The \"info_trivial\" tactic" ++ spc () + ++strbrk"does not print traces anymore." ++ spc() + ++strbrk"Use \"Info 1 trivial\", instead.") + end; Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1984,6 +1990,12 @@ and interp_atomic ist tac : unit Proofview.tactic = (Option.map (List.map (interp_hint_base ist)) l)) end | TacAuto (debug,n,lems,l) -> + begin if debug == Tacexpr.Info then + msg_warning + (strbrk"The \"info_auto\" tactic" ++ spc () + ++strbrk"does not print traces anymore." ++ spc() + ++strbrk"Use \"Info 1 auto\", instead.") + end; Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in -- cgit v1.2.3 From 15a3b57db10e61c9de12b5880b04b46db1494b5b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 26 Feb 2015 14:31:25 +0100 Subject: Fixing printing of ordinals. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 013270b0bd..ccf4795d68 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -882,7 +882,7 @@ let msg_quantified_hypothesis = function | NamedHyp id -> str "quantified hypothesis named " ++ pr_id id | AnonHyp n -> - int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++ + pr_nth n ++ str " non dependent hypothesis" let depth_of_quantified_hypothesis red h gl = -- cgit v1.2.3 From 31846ce3bb4053a4fd121afd6aa8260b0c5dff18 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 26 Feb 2015 17:08:43 +0100 Subject: Fixing bug #3298. --- tactics/eauto.ml4 | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'tactics') diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 30c5e686a9..3d98bc6e19 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -125,6 +125,14 @@ let unify_e_resolve poly flags (c,clenv) gls = tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls +let hintmap_of hdc concl = + match hdc with + | None -> fun db -> Hint_db.map_none db + | Some hdc -> + if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db) + else (fun db -> Hint_db.map_auto hdc concl db) + (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) + let e_exact poly flags (c,clenv) = let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv @@ -145,16 +153,11 @@ let rec e_trivial_fail_db db_list local_db goal = tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = + let hint_of_db = hintmap_of hdc concl in let hintl = - if occur_existential concl then List.map_append (fun db -> let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db) - (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list) - else - List.map_append (fun db -> - let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list) + List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) in let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> @@ -175,17 +178,14 @@ and e_my_find_search db_list local_db hdc concl = List.map tac_of_hint hintl and e_trivial_resolve db_list local_db gl = - try - priority - (e_my_find_search db_list local_db - (decompose_app_bound gl) gl) - with Bound | Not_found -> [] + let hd = try Some (decompose_app_bound gl) with Bound -> None in + try priority (e_my_find_search db_list local_db hd gl) + with Not_found -> [] let e_possible_resolve db_list local_db gl = - try List.map snd - (e_my_find_search db_list local_db - (decompose_app_bound gl) gl) - with Bound | Not_found -> [] + let hd = try Some (decompose_app_bound gl) with Bound -> None in + try List.map snd (e_my_find_search db_list local_db hd gl) + with Not_found -> [] let find_first_goal gls = try first_goal gls with UserError _ -> assert false -- cgit v1.2.3