wit_tactic top type is tacvalue

Author: SkySkimmer

plugins/firstorder/g_ground.mlg

@@ -61,7 +61,7 @@ let gen_ground_tac ist taco ids bases =
   Proofview.Goal.enter begin fun gl ->
       let solver=
         match taco with
-        | Some tac -> tactic_of_value ist tac
+        | Some tac -> tactic_of_tacvalue ist tac
         | None-> default_solver ()
       in
       let startseq k =

plugins/ltac/extraargs.mlg

@@ -266,11 +266,15 @@ let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
     | None -> mt ()
     | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t)
 
+let top_pr_by_arg_tac env sigma prc prlc _prtac opt_c =
+  pr_by_arg_tac env sigma prc prlc (fun env _ _ t -> Pptactic.pr_tacvalue env t) opt_c
 }
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic option
-  PRINTED BY { pr_by_arg_tac env sigma }
+  PRINTED BY { top_pr_by_arg_tac env sigma }
+  RAW_PRINTED BY { pr_by_arg_tac env sigma }
+  GLOB_PRINTED BY { pr_by_arg_tac env sigma }
 | [ "by" tactic3(c) ] -> { Some c }
 | [ ] -> { None }
 END

plugins/ltac/extraargs.mli

@@ -57,7 +57,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Procq.Entry.t
 val wit_by_arg_tac :
   (raw_tactic_expr option,
   glob_tactic_expr option,
-  Geninterp.Val.t option) Genarg.genarg_type
+  tacvalue option) Genarg.genarg_type
 
 val pr_by_arg_tac :
   Environ.env -> Evd.evar_map ->

plugins/ltac/extratactics.mlg

@@ -31,7 +31,7 @@ DECLARE PLUGIN "rocq-runtime.plugins.ltac"
 
 TACTIC EXTEND assert_succeeds
 | [ "assert_succeeds" tactic3(tac) ]
-  -> { Internals.assert_succeeds (Tacinterp.tactic_of_value ist tac) }
+  -> { Internals.assert_succeeds (Tacinterp.tactic_of_tacvalue ist tac) }
 END
 
 TACTIC EXTEND replace
@@ -179,24 +179,24 @@ TACTIC EXTEND autorewrite
     { auto_multi_rewrite  l ( cl) }
 | [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
     {
-      auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
+      auto_multi_rewrite_with (Tacinterp.tactic_of_tacvalue ist t) l cl
    }
 END
 
 TACTIC EXTEND autorewrite_star
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
     { auto_multi_rewrite ~conds:AllMatches l cl }
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
-  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl }
+  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_tacvalue ist t) l cl }
 END
 
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
 {
 
-let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
-  let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
+let rewrite_star ist clause orient occs c (tac : Tacexpr.tacvalue option) =
+  let tac' = Option.map (fun t -> Tacinterp.tactic_of_tacvalue ist t, FirstSolved) tac in
   Internals.with_delayed_uconstr ist c
     (fun c -> general_rewrite ~where:clause ~l2r:orient occs ?tac:tac' ~freeze:true ~dep:true ~with_evars:true (c,NoBindings))
 
@@ -420,12 +420,12 @@ let add_transitivity_lemma left lem =
 (* Vernacular syntax *)
 
 TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) }
+| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_tacvalue ist tac) }
 | ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) }
 END
 
 TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) }
+| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_tacvalue ist tac) }
 | ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) }
 END
 
@@ -472,9 +472,9 @@ END
 
 TACTIC EXTEND transparent_abstract
 | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
-    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; }
+    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_tacvalue ist t) end; }
 | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
-    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; }
+    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_tacvalue ist t) end; }
 END
 
 (* ********************************************************************* *)
@@ -683,6 +683,6 @@ END
 
 TACTIC EXTEND with_strategy
 | [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
-  with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
+  with_set_strategy [(v, q)] (Tacinterp.tactic_of_tacvalue ist tac)
 }
 END

plugins/ltac/internals.ml

@@ -53,7 +53,7 @@ let with_delayed_uconstr ist c tac =
 
 let replace_in_clause_maybe_by ist dir_opt c1 c2 cl tac =
   with_delayed_uconstr ist c1
-  (fun c1 -> Equality.replace_in_clause_maybe_by dir_opt c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
+  (fun c1 -> Equality.replace_in_clause_maybe_by dir_opt c1 c2 cl (Option.map (Tacinterp.tactic_of_tacvalue ist) tac))
 
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> Equality.replace_term dir_opt c cl)
@@ -163,7 +163,7 @@ let is_const x =
     | _ -> Tacticals.tclFAIL (Pp.str "not a constant")
 
 let unshelve ist t =
-  Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
+  Proofview.with_shelf (Tacinterp.tactic_of_tacvalue ist t) >>= fun (gls, ()) ->
   let gls = List.map Proofview.with_empty_state gls in
   Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
   Proofview.Unsafe.tclSETGOALS (gls @ ogls)

plugins/ltac/internals.mli

@@ -30,7 +30,7 @@ val with_delayed_uconstr : Tacinterp.interp_sign ->
   closed_glob_constr -> (EConstr.constr -> unit tactic) -> unit tactic
 val replace_in_clause_maybe_by : Tacinterp.interp_sign -> bool option ->
   closed_glob_constr -> EConstr.constr ->
-  Locus.clause -> Tacinterp.Value.t option -> unit tactic
+  Locus.clause -> Tacexpr.tacvalue option -> unit tactic
 val replace_term : Tacinterp.interp_sign -> bool option -> closed_glob_constr ->
   Locus.clause -> unit tactic
 
@@ -51,7 +51,7 @@ val is_constructor : EConstr.t -> unit tactic
 val is_proj : EConstr.t -> unit tactic
 val is_const : EConstr.t -> unit tactic
 
-val unshelve : Tacinterp.interp_sign -> Tacinterp.Value.t -> unit tactic
+val unshelve : Tacinterp.interp_sign -> Tacexpr.tacvalue -> unit tactic
 
 val decompose : EConstr.t list -> EConstr.t -> unit tactic
 

plugins/ltac/pptactic.ml

@@ -91,7 +91,7 @@ type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
@@ -112,7 +112,7 @@ type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   entry_relative_level -> 'a -> Pp.t
 
 let string_of_genarg_arg (ArgumentType arg) =
@@ -1400,9 +1400,25 @@ let () =
   register_basic_print0 Stdarg.wit_pre_ident str str str;
   register_basic_print0 Stdarg.wit_string qstring qstring qstring
 
+let pr_tacvalue env = function
+  | VFun (a,_,loc,ids,l,tac) ->
+    let open Pp in
+    let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in
+    let pr_env env =
+      if Id.Map.is_empty ids then mt ()
+      else
+        cut () ++ str "where" ++
+        Id.Map.fold (fun id c pp ->
+            cut () ++ Id.print id ++ str " := " ++ pr_value ltop c ++ pp)
+          ids (mt ())
+    in
+    v 0 (hov 0 (pr_glob_tactic env tac) ++ pr_env env)
+  | VRec _ -> str "<tactic closure>"
+
 let () =
   let printer env sigma _ _ prtac = prtac env sigma in
-  declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
+  let top_print env sigma _ _ _ _ = pr_tacvalue env in
+  declare_extra_genarg_pprule_with_level wit_tactic printer printer top_print
   ltop (LevelLe 0)
 
 let () =

plugins/ltac/pptactic.mli

@@ -42,7 +42,7 @@ type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
@@ -63,7 +63,7 @@ type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   entry_relative_level -> 'a -> Pp.t
 
 val declare_extra_genarg_pprule :
@@ -155,6 +155,8 @@ val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
 
 val pr_value : entry_relative_level -> Val.t -> Pp.t
 
+val pr_tacvalue : env -> tacvalue -> Pp.t
+
 val pp_ltac_call_kind : ltac_call_kind -> Pp.t
 
 val ltop : entry_relative_level

plugins/ltac/tacarg.ml

@@ -27,7 +27,7 @@ let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
 let wit_bindings = make0 "bindings"
 let wit_quantified_hypothesis = wit_quant_hyp
 
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type =
   make0 "tactic"
 
 let wit_ltac_in_term = GenConstr.create "ltac_in_term"

plugins/ltac/tacarg.mli

@@ -42,7 +42,7 @@ val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
 
 (** Generic arguments based on Ltac. *)
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type
 
 val wit_ltac_in_term : (raw_tactic_expr, Names.Id.Set.t * glob_tactic_expr) GenConstr.tag