aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extraargs.mli2
-rw-r--r--plugins/ltac/extratactics.ml424
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacintern.ml15
-rw-r--r--plugins/ltac/tacinterp.ml38
-rw-r--r--plugins/ltac/tacinterp.mli5
10 files changed, 58 insertions, 38 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 6097951330..89feea8dcf 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -249,7 +249,7 @@ END
let pr_by_arg_tac _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b06f35ddc4..00668ddc7d 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -64,7 +64,7 @@ val wit_by_arg_tac :
Geninterp.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
- (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f3f2f27e9e..99e4440102 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac =
fail_evar = false;
expand_evars = true
} in
- let c = Pretyping.type_uconstr ~flags ist c in
+ let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
let replace_in_clause_maybe_by ist c1 c2 cl tac =
@@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c =
let flags =
{ constr_flags () with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
- let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
+ let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
let update = begin fun sigma ->
c env sigma
end in
@@ -626,19 +626,19 @@ END
let subst_var_with_hole occ tid t =
let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
let locref = ref 0 in
- let rec substrec = function
- | { CAst.v = GVar id } as x ->
+ let rec substrec x = match DAst.get x with
+ | GVar id ->
if Id.equal id tid
then
(decr occref;
if Int.equal !occref 0 then x
else
(incr locref;
- CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+ DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
Misctypes.IntroAnonymous, None)))
else x
- | c -> map_glob_constr_left_to_right substrec c in
+ | _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
in
if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
@@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t =
let subst_hole_with_term occ tc t =
let locref = ref 0 in
let occref = ref occ in
- let rec substrec = function
- | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
+ let rec substrec c = match DAst.get c with
+ | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
- CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+ DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
- | c -> map_glob_constr_left_to_right substrec c
+ | _ -> map_glob_constr_left_to_right substrec c
in
substrec t
@@ -666,8 +666,8 @@ let hResolve id c occ t =
let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
let concl = Proofview.Goal.concl gl in
let env_ids = Termops.ids_of_context env in
- let c_raw = Detyping.detype true env_ids env sigma c in
- let t_raw = Detyping.detype true env_ids env sigma t in
+ let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
+ let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
let rec resolve_hole t_hole =
try
Pretyping.understand env sigma t_hole
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 301943a509..5baa0d5c1d 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -48,7 +48,7 @@ let eval_uconstrs ist cs =
expand_evars = true
} in
let map c env sigma = c env sigma in
- List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
+ List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c874f8d5a3..c22e683235 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ END
let clsubstitute o c =
Proofview.Goal.enter begin fun gl ->
- let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
+ let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
let hyps = Tacmach.New.pf_ids_of_hyps gl in
Tacticals.New.tclMAP
(fun cl ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 140cc33440..f4e3ba633f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Geninterp
open Stdarg
open Tacarg
open Libnames
-open Ppextend
+open Notation_term
open Misctypes
open Locus
open Decl_kinds
@@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer =
let strip_prod_binders_glob_constr n (ty,_) =
let rec strip_ty acc n ty =
if Int.equal n 0 then (List.rev acc, (ty,None)) else
- match ty.CAst.v with
+ match DAst.get ty with
Glob_term.GProd(na,Explicit,a,b) ->
strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0bf9bc7f62..1f6ebaf448 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,7 @@ open Misctypes
open Environ
open Constrexpr
open Tacexpr
-open Ppextend
+open Notation_term
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0554d43641..fc6ee6aab6 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -106,12 +106,12 @@ let intern_ltac_variable ist = function
let intern_constr_reference strict ist = function
| Ident (_,id) as r when not strict && find_hyp id ist ->
- (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
+ (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
| Ident (_,id) as r when find_var id ist ->
- (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+ (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
| r ->
let loc,_ as lqid = qualid_of_reference r in
- CAst.make @@ GRef (locate_global_with_alias lqid,None),
+ DAst.make @@ GRef (locate_global_with_alias lqid,None),
if strict then None else Some (CAst.make @@ CRef (r,None))
(* Internalize an isolated reference in position of tactic *)
@@ -264,9 +264,10 @@ let intern_destruction_arg ist = function
| clear,ElimOnIdent (loc,id) ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
- match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
- | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
- | c -> clear,ElimOnConstr (c,NoBindings)
+ let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
+ match DAst.get c with
+ | GVar id -> clear,ElimOnIdent (c.CAst.loc,id)
+ | _ -> clear,ElimOnConstr ((c, p), NoBindings)
else
clear,ElimOnIdent (loc,id)
@@ -348,7 +349,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
ltac_extra = ist.extra;
} in
let c = Constrintern.interp_reference sign r in
- match c.CAst.v with
+ match DAst.get c with
| GRef (r,None) ->
Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
| GVar id ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d3e625e73a..8fa95ffb02 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) =
(* Interprets a constr expression *)
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
let try_expand_ltac_var sigma x =
- try match dest_fun x with
- | { CAst.v = GVar id }, _ ->
+ try match DAst.get (fst (dest_fun x)) with
+ | GVar id ->
let v = Id.Map.find id ist.lfun in
sigma, List.map inj_fun (coerce_to_constr_list env v)
| _ ->
@@ -689,7 +689,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
(* dest_fun, List.assoc may raise Not_found *)
let sigma, c = interp_fun ist env sigma x in
sigma, [c] in
- let sigma, l = List.fold_map try_expand_ltac_var sigma l in
+ let sigma, l = List.fold_left_map try_expand_ltac_var sigma l in
sigma, List.flatten l
let interp_constr_list ist env sigma c =
@@ -908,18 +908,18 @@ and interp_intro_pattern_action ist env sigma = function
and interp_or_and_intro_pattern ist env sigma = function
| IntroAndPattern l ->
- let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_intro_pattern ist env) sigma l in
sigma, IntroAndPattern l
| IntroOrPattern ll ->
- let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in
+ let sigma, ll = List.fold_left_map (interp_intro_pattern_list_as_list ist env) sigma ll in
sigma, IntroOrPattern ll
and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
(try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
- List.fold_map (interp_intro_pattern ist env) sigma l)
- | l -> List.fold_map (interp_intro_pattern ist env) sigma l
+ List.fold_left_map (interp_intro_pattern ist env) sigma l)
+ | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
let interp_intro_pattern_naming_option ist env sigma = function
| None -> None
@@ -973,7 +973,7 @@ let interp_bindings ist env sigma = function
let sigma, l = interp_open_constr_list ist env sigma l in
sigma, ImplicitBindings l
| ExplicitBindings l ->
- let sigma, l = List.fold_map (interp_binding ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in
sigma, ExplicitBindings l
let interp_constr_with_bindings ist env sigma (c,bl) =
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
if Tactics.is_quantified_hypothesis id gl then
keep,ElimOnIdent (loc,id)
else
- let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+ let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
let f env sigma =
let (sigma,c) = interp_open_constr ist env sigma c in
(sigma, (c,NoBindings))
@@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function
:: read_match_rule lfun ist env sigma tl
| [] -> []
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+ ?(expected_type = WithoutTypeConstraint) ist c =
+ begin fun env sigma ->
+ let { closure; term } = c in
+ let vars = {
+ ltac_constrs = closure.typed;
+ ltac_uconstrs = closure.untyped;
+ ltac_idents = closure.idents;
+ ltac_genargs = Id.Map.empty;
+ } in
+ understand_ltac flags env sigma vars expected_type term
+ end
+
let warn_deprecated_info =
CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
(fun () ->
@@ -1657,7 +1671,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
- let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in
+ let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in
let named_tac =
let tac = Tactics.elim ev keep cb cbo in
name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
@@ -1775,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
- List.fold_map begin fun sigma (c,(ipato,ipats),cls) ->
+ List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) ->
(* TODO: move sigma as a side-effect *)
(* spiwack: the [*p] variants are for printing *)
let cp = c in
@@ -1789,7 +1803,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let l,lp = List.split l in
let sigma,el =
- Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in
+ Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(name_atomic ~env
(TacInductionDestruct(isrec,ev,(lp,el)))
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 73e4f3d6ab..c1ab2b4c49 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -54,6 +54,11 @@ val set_debug : debug_info -> unit
(** Gives the state of debug *)
val get_debug : unit -> debug_info
+val type_uconstr :
+ ?flags:Pretyping.inference_flags ->
+ ?expected_type:Pretyping.typing_constraint ->
+ Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+
(** Adds an interpretation function for extra generic arguments *)
val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:02:41 +0000