aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml442
-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, 43 insertions, 42 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b847aadf2..b4c6f9c90 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -403,38 +403,38 @@ open Leminv
let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
-VERNAC ARGUMENT EXTEND sort
-| [ "Set" ] -> [ GSet ]
-| [ "Prop" ] -> [ GProp ]
-| [ "Type" ] -> [ GType [] ]
-END
+(*VERNAC ARGUMENT EXTEND sort_family
+| [ "Set" ] -> [ InSet ]
+| [ "Prop" ] -> [ InProp ]
+| [ "Type" ] -> [ InType ]
+END*)
VERNAC COMMAND EXTEND DeriveInversionClear
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
-> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ]
+ -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
END
VERNAC COMMAND EXTEND DeriveInversion
-| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
-> [ add_inversion_lemma_exn na c s false inv_tac ]
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c GProp false inv_tac ]
+ -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
END
VERNAC COMMAND EXTEND DeriveDependentInversion
-| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
-> [ add_inversion_lemma_exn na c s true dinv_tac ]
END
VERNAC COMMAND EXTEND DeriveDependentInversionClear
-| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
-> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
END
@@ -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 c874f8d5a..c22e68323 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 cb7d9b9c0..f4e3ba633 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 0554d4364..fc6ee6aab 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 51eed2f4e..8fa95ffb0 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.39.1) at 2024-07-04 20:53:12 +0000