Merge branch 'v8.6'

4 files changed, 15 insertions, 12 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index cadd7ef2c9..23ce5fb4ea 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -262,7 +262,8 @@ let add_rewrite_hint bases ort t lcsr =
     let ctx =
       let ctx = UState.context_set ctx in
         if poly then ctx
-	else (Global.push_context_set false ctx; Univ.ContextSet.empty)
+	else (Declare.declare_universe_context false ctx;
+              Univ.ContextSet.empty)
     in
       Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
   let eqs = List.map f lcsr in
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index d128b4d086..54229bb2ae 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -48,7 +48,6 @@ let new_entry name =
   let e = Gram.entry_create name in
   e
 
-let selector = new_entry "vernac:selector"
 let toplevel_selector = new_entry "vernac:toplevel_selector"
 let tacdef_body = new_entry "tactic:tacdef_body"
 
@@ -84,7 +83,7 @@ let warn_deprecated_appcontext =
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
-          tactic_mode constr_may_eval constr_eval selector toplevel_selector
+          tactic_mode constr_may_eval constr_eval toplevel_selector
           operconstr;
 
   tactic_then_last:
@@ -322,13 +321,16 @@ GEXTEND Gram
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
           Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
   ;
+  selector_body:
+  [ [ l = range_selector_or_nth -> l
+    | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ]
+  ;
   selector:
-    [ [ l = range_selector_or_nth; ":" -> l
-      | IDENT "all" ; ":" -> SelectAll ] ]
+    [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ]
   ;
   toplevel_selector:
-    [ [ s = selector -> s
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ]
+    [ [ sel = selector_body; ":" -> sel
+    |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
     [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 102918e5e5..2514ededb0 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -128,7 +128,7 @@ let to_ltacprof_results xml =
   | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML")
 
 let feedback_results results =
-  Feedback.(feedback 
+  Feedback.(feedback
     (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results)))
 
 (* ************** pretty printing ************************************* *)
@@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
-  let filter s n = filter s && n >= cutoff in
+  let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
@@ -401,11 +401,11 @@ let print_results ~cutoff =
   print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~cutoff:0.0 ~filter:(fun s ->
+  print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s ->
     String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
 
 let do_print_results_at_close () =
-  if get_profiling () then print_results ~cutoff:0.0
+  if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index 9083bda60a..8cb76d81c5 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ]
 | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
 END