aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg4
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_class.mlg12
-rw-r--r--plugins/ltac/g_ltac.mlg50
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/leminv.ml3
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml74
-rw-r--r--plugins/ltac/taccoerce.ml28
-rw-r--r--plugins/ltac/tacentries.ml55
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml30
-rw-r--r--plugins/ltac/tacinterp.mli6
-rw-r--r--plugins/ltac/tacsubst.ml2
19 files changed, 121 insertions, 167 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index f1f538ab39..b7ac71181a 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -20,8 +20,6 @@ open Tacarg
open Names
open Logic
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 863c4d37d8..ad4374dba3 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -47,7 +47,7 @@ let () =
let () =
let register name entry = Tacentries.register_tactic_notation_entry name entry in
- register "hyp" wit_var;
+ register "hyp" wit_hyp;
register "simple_intropattern" wit_simple_intropattern;
register "integer" wit_integer;
register "reference" wit_ref;
@@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences
GLOB_PRINTED BY { pr_occurrences }
| [ ne_integer_list(l) ] -> { ArgArg l }
-| [ var(id) ] -> { ArgVar id }
+| [ hyp(id) ] -> { ArgVar id }
END
{
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4f20e5a800..a2a47c0bf4 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -33,8 +33,6 @@ open Proofview.Notations
open Attributes
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
@@ -450,7 +448,7 @@ END
(* Subst *)
TACTIC EXTEND subst
-| [ "subst" ne_var_list(l) ] -> { subst l }
+| [ "subst" ne_hyp_list(l) ] -> { subst l }
| [ "subst" ] -> { subst_all () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 2e72ceae5a..44472a1995 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -18,8 +18,6 @@ open Pcoq.Constr
open Pltac
open Hints
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..8c2e633be5 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -31,12 +31,12 @@ let set_transparency cl b =
}
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Transparent" reference_list(cl) ] -> {
+| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
set_transparency cl true }
END
VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Opaque" reference_list(cl) ] -> {
+| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
set_transparency cl false }
END
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
@@ -87,11 +87,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
- { typeclasses_eauto ~strategy:Bfs ~depth:d l }
+ { typeclasses_eauto ~depth:d ~strategy:Bfs l }
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
+ typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index be0d71ad46..6cf5d30a95 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram
open Stdarg
open Tacarg
open Vernacextend
-open Goptions
open Libnames
-let print_info_trace =
- declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
-
-let vernac_solve ~pstate n info tcom b =
- let open Goal_select in
- let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
- let with_end_tac = if b then Some etac else None in
- let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info (print_info_trace ()) in
- let (p,status) =
- Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
- in
- (* in case a strict subtree was completed,
- go back to the top of the prooftree *)
- let p = Proof.maximal_unfocus Vernacentries.command_focus p in
- p,status) pstate in
- if not status then Feedback.feedback Feedback.AddedAxiom;
- pstate
-
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
}
@@ -409,34 +389,34 @@ END
{
-let is_anonymous_abstract = function
- | TacAbstract (_,None) -> true
- | TacSolve [TacAbstract (_,None)] -> true
- | _ -> false
let rm_abstract = function
- | TacAbstract (t,_) -> t
- | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
- | x -> x
+ | TacAbstract (t,_) -> t, true
+ | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true
+ | x -> x, false
let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- vernac_solve g n t def
+ let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+ ComTactic.solve g ~info t ~with_end_tac
}
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+END
+
+VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
+| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{
- let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
- let parallel = `Yes (solving_tac,anon_abstracting_tac) in
let pbr = if solving_tac then Some "par" else None in
- VtProofStep{ parallel = parallel; proof_block_detection = pbr }
+ VtProofStep{ proof_block_detection = pbr }
} -> {
- let t = rm_abstract t in
- vernac_solve Goal_select.SelectAll n t def
+ let t, abstract = rm_abstract t in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+ ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
}
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fc24475a62..6bf330c830 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -111,6 +111,8 @@ END
VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
+| [ "Solve" "Obligations" "of" ident(name) ] ->
+ { try_solve_obligations (Some name) None }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
{ try_solve_obligations None (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" ] ->
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 8331927cda..ee94fd565a 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -29,8 +29,6 @@ open Pvernac.Vernac_
open Pltac
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..c186a83a5c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
| "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> { IntroFresh prefix }
+ [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
| "?" -> { IntroAnonymous }
| id = ident -> { IntroIdentifier id } ] ]
;
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 47df3ec34f..f42c1f73a3 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -245,7 +245,8 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let add_inversion_lemma_exn ~poly na com comsort bool tac =
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+ let c, uctx = Constrintern.interp_type env sigma com in
+ let sigma = Evd.from_ctx uctx in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
add_inversion_lemma ~poly na env sigma c sort bool tac
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 85bb901046..fe896f9351 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
@@ -1323,7 +1323,7 @@ let () =
register_basic_print0 wit_smart_global
(pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
- register_basic_print0 wit_var pr_lident pr_lident pr_id;
+ register_basic_print0 wit_hyp pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
Genprint.register_print0
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0dbf16a821..9c15d24dd3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -146,7 +146,7 @@ let header =
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
- h 0 (
+ h (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
@@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node =
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))) ++
+ h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8de6cbc0a6..9bb435f4dc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -498,7 +498,7 @@ let rec decompose_app_rel env evd t =
let decompose_app_rel env evd t =
let (rel, t1, t2) = decompose_app_rel env evd t in
- let ty = Retyping.get_type_of env evd rel in
+ let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in
let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
(rel, t1, t2)
@@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with
let poly_subrelation sort =
if sort then PropGlobal.subrelation else TypeGlobal.subrelation
-let resolve_subrelation env avoid car rel sort prf rel' res =
+let resolve_subrelation env car rel sort prf rel' res =
if Termops.eq_constr (fst res.rew_evars) rel rel' then res
else
let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
@@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res =
rew_prf = RewPrf (rel', appsub);
rew_evars = evars }
-let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
+let resolve_morphism env m args args' (b,cstr) evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
@@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let proof = applist (proj, List.rev projargs) in
let newt = applist (m', List.rev typeargs) in
match respars with
- [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
+ [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt
| _ -> assert(false)
-let apply_constraint env avoid car rel prf cstr res =
+let apply_constraint env car rel prf cstr res =
match snd cstr with
| None -> res
- | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
+ | Some r -> resolve_subrelation env car rel (fst cstr) prf r res
-let coerce env avoid cstr res =
+let coerce env cstr res =
let evars, (rel, prf) = get_rew_prf res.rew_evars res in
let res = { res with rew_evars = evars } in
- apply_constraint env avoid res.rew_car rel prf cstr res
+ apply_constraint env res.rew_car rel prf cstr res
let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
@@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy =
then List.mem occ occs
else not (List.mem occ occs)
in
- { strategy = fun { state = occ ; env ; unfresh ;
+ { strategy = fun { state = occ ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
match unif with
@@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy =
else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
- let res = Success (coerce env unfresh cstr res) in
+ let res = Success (coerce env cstr res) in
(occ, res)
}
@@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
- let evars', prf, car, rel, c1, c2 =
- resolve_morphism env unfresh t m args args' (prop, cstr') evars'
+ let evars', prf, car, rel, c2 =
+ resolve_morphism env m args args' (prop, cstr') evars'
in
- let res = { rew_car = ty; rew_from = c1;
+ let res = { rew_car = ty; rew_from = t;
rew_to = c2; rew_prf = RewPrf (rel, prf);
rew_evars = evars' }
in Success res
@@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env unfresh res.rew_car
+ Success (apply_constraint env res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> res
in state, res
- (* if x' = None && flags.under_lambdas then *)
- (* let lam = mkLambda (n, x, b) in *)
- (* let lam', occ = aux env lam occ None in *)
- (* let res = *)
- (* match lam' with *)
- (* | None -> None *)
- (* | Some (prf, (car, rel, c1, c2)) -> *)
- (* Some (resolve_morphism env sigma t *)
- (* ~fnewt:unfold_all *)
- (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
- (* cstr evars) *)
- (* in res, occ *)
- (* else *)
-
| Prod (n, dom, codom) ->
let lam = mkLambda (n, dom, codom) in
let (evars', app), unfold =
@@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
dependent relations and using projections to get them out.
*)
- (* | Lambda (n, t, b) when flags.under_lambdas -> *)
- (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
- (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
- (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
- (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
- (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
- (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
- (* (match b' with *)
- (* | Some (Some r) -> *)
- (* let prf = match r.rew_prf with *)
- (* | RewPrf (rel, prf) -> *)
- (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
- (* let prf = mkLambda (n', t, prf) in *)
- (* RewPrf (rel, prf) *)
- (* | x -> x *)
- (* in *)
- (* Some (Some { r with *)
- (* rew_prf = prf; *)
- (* rew_car = mkProd (n, t, r.rew_car); *)
- (* rew_from = mkLambda(n, t, r.rew_from); *)
- (* rew_to = mkLambda (n, t, r.rew_to) }) *)
- (* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh = match n'.binder_name with
+ | Anonymous -> unfresh
+ | Name id -> Id.Set.add id unfresh
+ in
let open Context.Rel.Declaration in
let env' = EConstr.push_rel (LocalAssum (n', t)) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
@@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Success r ->
let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env unfresh (prop,cstr) res)
+ state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
let res =
match res with
- | Success r -> Success (coerce env unfresh (prop,cstr) r)
+ | Success r -> Success (coerce env (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
@@ -2144,7 +2112,7 @@ let setoid_proof ty fn fallback =
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
- with e ->
+ with e when CErrors.noncritical e ->
(* XXX what is the right test here as to whether e can be converted ? *)
let e, info = Exninfo.capture e in
Proofview.tclZERO ~info e
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index f7037176d2..ee28229cb7 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v =
match out_gen (topwit wit_intro_pattern) v with
| { CAst.v=IntroNaming (IntroIdentifier id)} -> id
| _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ else if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else match Value.to_constr v with
| None -> fail ()
| Some c ->
@@ -184,8 +184,8 @@ let id_of_name = function
| Some (IntroNaming (IntroIdentifier id)) -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else
match Value.to_constr v with
| None -> fail ()
@@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v =
match is_intro_pattern v with
| Some pat -> pat
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
| Some c when isVar sigma c ->
@@ -259,8 +259,8 @@ let coerce_to_constr env v =
([], c)
else if has_type v (topwit wit_constr_under_binders) then
out_gen (topwit wit_constr_under_binders) v
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
(try [], constr_of_id env id with Not_found -> fail ())
else fail ()
@@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
else fail ()
else if has_type v (topwit wit_ref) then
@@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if is_variable env id then id else fail ()
else match Value.to_constr v with
| Some c when isVar sigma c -> destVar sigma c
@@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v =
| Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id
| Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
NamedHyp id
else if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f0ca813b08..6823b6411f 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -31,18 +31,6 @@ type argument = Genarg.ArgT.any Extend.user_symbol
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
let atactic n =
if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
@@ -70,28 +58,37 @@ let check_separator ?loc = function
| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
let rec parse_user_entry ?loc s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+ let open CString in
+ let matches pre suf s =
+ String.length s > (String.length pre + String.length suf) &&
+ is_prefix pre s && is_suffix suf s
+ in
+ let basename pre suf s =
+ let plen = String.length pre in
+ String.sub s plen (String.length s - (plen + String.length suf))
+ in
+ let tactic_len = String.length "tactic" in
+ if matches "ne_" "_list" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in
check_separator ?loc sep;
Ulist1 entry
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
+ else if matches "ne_" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in
Ulist1sep (entry, get_separator sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+ else if matches "" "_list" s then
+ let entry = parse_user_entry ?loc (basename "" "_list" s) None in
check_separator ?loc sep;
Ulist0 entry
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
+ else if matches "" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in
Ulist0sep (entry, get_separator sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+ else if matches "" "_opt" s then
+ let entry = parse_user_entry ?loc (basename "" "_opt" s) None in
check_separator ?loc sep;
Uopt entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
- let n = Char.code s.[6] - 48 in
+ else if String.length s = tactic_len + 1 && is_prefix "tactic" s
+ && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then
+ let n = Char.code s.[tactic_len] - Char.code '0' in
check_separator ?loc sep;
Uentryl ("tactic", n)
else
@@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function
EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
- assert (coincide (ArgT.repr tag) "tactic" 0);
+ assert (CString.is_suffix "tactic" (ArgT.repr tag));
get_tacentry n lev
(** Tactic grammar extensions *)
@@ -219,7 +216,9 @@ let interp_prod_item = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
else begin match ArgT.name s with
- | None -> user_err Pp.(str ("Unknown entry "^s^"."))
+ | None ->
+ if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *)
+ else user_err Pp.(str ("Unknown entry "^s^"."))
| Some arg -> arg
end
| Some n ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index dea216045e..9c3b05fdf1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -835,7 +835,7 @@ let () =
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
- Genintern.register_intern0 wit_var (lift intern_hyp);
+ Genintern.register_intern0 wit_hyp (lift intern_hyp);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
Genintern.register_intern0 wit_ltac (lift intern_ltac);
Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff6a36a049..12bfb4d09e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg =
match v with
| {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
| _ -> error ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
try_cast_id id
else if has_type v (topwit wit_int) then
keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
@@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
| ArgVar {loc;v=id} ->
let v =
try Id.Map.find id ist.lfun
- with Not_found -> in_gen (topwit wit_var) id
+ with Not_found -> in_gen (topwit wit_hyp) id
in
let open Ftactic in
force_vrec ist v >>= begin fun v ->
@@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
let open Ftactic.Notations in
(* Ad-hoc handling of some types. *)
let tag = genarg_tag x in
- if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
+ if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then
interp_genarg_var_list ist x
else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
interp_genarg_constr_list ist x
@@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x =
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
+ let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in
let lc = interp_hyp_list ist env sigma lc in
- let lc = in_list (val_tag wit_var) lc in
+ let lc = in_list (val_tag wit_hyp) lc in
Ftactic.return lc
end
@@ -1996,16 +1996,20 @@ let interp_tac_gen lfun avoid_ids debug t =
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
+(* MUST be marshallable! *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
+
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
-let hide_interp global t ot =
+let hide_interp {global;ast} =
let hide_interp env =
let ist = Genintern.empty_glob_sign env in
- let te = intern_pure_tactic ist t in
+ let te = intern_pure_tactic ist ast in
let t = eval_tactic te in
- match ot with
- | None -> t
- | Some t' -> Tacticals.New.tclTHEN t t'
+ t
in
if global then
Proofview.tclENV >>= fun env ->
@@ -2015,6 +2019,8 @@ let hide_interp global t ot =
hide_interp (Proofview.Goal.env gl)
end
+let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+
(***************************************************************************)
(** Register standard arguments *)
@@ -2090,7 +2096,7 @@ let () =
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
- register_interp0 wit_var (lift interp_hyp);
+ register_interp0 wit_hyp (lift interp_hyp);
register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
register_interp0 wit_clause_dft_concl (lift interp_clause);
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index cbb17bf0fa..01d7306c9d 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
-val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+val hide_interp : tactic_expr ComTactic.tactic_interpreter
(** Internals that can be useful for syntax extensions. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fd869b225f..ec44ae4698 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -282,7 +282,7 @@ let () =
Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
- Genintern.register_subst0 wit_var (fun _ v -> v);
+ Genintern.register_subst0 wit_hyp (fun _ v -> v);
Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
Genintern.register_subst0 wit_tactic subst_tactic;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:05:26 +0000