aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml420
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/tacintern.ml15
-rw-r--r--plugins/ltac/tacinterp.ml24
5 files changed, 32 insertions, 31 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b847aadf21..99e4440102 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -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_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 cb7d9b9c02..f4e3ba633f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -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/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 51eed2f4ec..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))
@@ -1671,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
@@ -1789,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
@@ -1803,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)))
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:02:41 +0000