From 5ecd8a6a5593d7f197a115b129ebd5f530e40161 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 8 Sep 2016 23:44:44 +0200 Subject: Fix bug #3920 for good after 44ada64. The previous commit did not apply the beta reduction for compatibility on the correct goal. We rather apply it on the first generated subgoal. This fixes the ergo contrib. --- ltac/rewrite.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index cf59b6dc1f..69f45e1aeb 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1578,11 +1578,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = | Some id, Some p -> let tac = tclTHENLIST [ Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; - beta_hyp id; Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> - assert_replacing id newt tac + tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> convert_hyp_no_check (LocalAssum (id, newt)) <*> -- cgit v1.2.3 From 345b6addf7195d39e86827aca9c16f0407aba028 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Sep 2016 15:43:17 -0700 Subject: Revert the LtacProf tactic table header This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.) --- ltac/profile_ltac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 3661fe54f2..50f9583f94 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -147,7 +147,7 @@ let rec list_iter_is_last f = function | x :: xs -> f false x :: list_iter_is_last f xs let header = - str " tactic local total calls max" ++ + str " tactic local total calls max " ++ fnl () ++ str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++ fnl () -- cgit v1.2.3 From 74d2ef26ce991c16039db8c06f813836304c6480 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 11 Sep 2016 15:49:50 -0700 Subject: Fix newlines in printout of LtacProf Previously, newlines were missing if a node had no children. --- ltac/profile_ltac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 50f9583f94..d2b7c70750 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -160,6 +160,7 @@ let rec print_node ~filter all_total indent prefix (s, e) = ++ padl 8 (string_of_int e.ncalls) ++ padl 10 (format_sec (e.max_total)) ) ++ + fnl () ++ print_table ~filter all_total indent false e.children and print_table ~filter all_total indent first_level table = @@ -179,7 +180,7 @@ and print_table ~filter all_total indent first_level table = let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in print_node ~filter all_total (indent ^ sep0) (indent ^ sep1) in - prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) + prlist (fun pr -> pr) (list_iter_is_last iter ls) let to_string ~filter node = let tree = node.children in @@ -224,7 +225,6 @@ let to_string ~filter node = header ++ print_table ~filter all_total "" true flat_tree ++ fnl () ++ - fnl () ++ header ++ print_table ~filter all_total "" true tree in -- cgit v1.2.3 From 93ae6db3375d442ef67154c832bbdf155cffe32f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Sep 2016 13:00:02 +0200 Subject: LtacProp: fix reset_profile (fix #5079) --- ltac/profile_ltac.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'ltac') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index d2b7c70750..fe591c7756 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -73,7 +73,7 @@ module Local = Summary.Local let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] -let reset_profile () = +let reset_profile_tmp () = Local.(stack := [empty_treenode root]); encountered_multi_success_backtracking := false @@ -295,7 +295,7 @@ let exit_tactic start_time c = | [] | [_] -> (* oops, our stack is invalid *) encounter_multi_success_backtracking (); - reset_profile () + reset_profile_tmp () | node :: (parent :: rest as full_stack) -> let name = string_of_call c in if not (String.equal name node.name) then @@ -330,7 +330,7 @@ let exit_tactic start_time c = (* Calls are over, we reset the stack and send back data *) if rest == [] && get_profiling () then begin assert(String.equal root parent.name); - reset_profile (); + reset_profile_tmp (); feedback_results parent end @@ -381,6 +381,10 @@ let _ = data := SM.add s (merge_roots results other_results) !data | _ -> ())) +let reset_profile () = + reset_profile_tmp (); + data := SM.empty + (* ******************** *) let print_results_filter ~filter = -- cgit v1.2.3 From 0e94cb62410354e5df4e65b34e7cbf8451b31d6e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Sep 2016 13:42:04 +0200 Subject: Fixing #5078 (wrong detection of evaluable local hypotheses). --- ltac/taccoerce.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'ltac') diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 0110510d35..46469df6a1 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -241,9 +241,8 @@ let coerce_to_evaluable_ref env v = | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id | _ -> fail () else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id - else fail () + let ev = EvalVarRef (out_gen (topwit wit_var) v) in + if Tacred.is_evaluable env ev then ev else fail () else if has_type v (topwit wit_ref) then let open Globnames in let r = out_gen (topwit wit_ref) v in -- cgit v1.2.3