aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/coretactics.ml426
-rw-r--r--ltac/extratactics.ml44
-rw-r--r--ltac/tacinterp.ml45
-rw-r--r--ltac/tauto.ml2
4 files changed, 37 insertions, 40 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 8b5f527cd0..ce28eacc09 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,15 +39,15 @@ TACTIC EXTEND cut
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+ [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
END
TACTIC EXTEND vm_cast_no_check
- [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ]
+ [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
END
TACTIC EXTEND native_cast_no_check
- [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ]
+ [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
END
TACTIC EXTEND casetype
@@ -200,10 +200,10 @@ END
(** Move *)
TACTIC EXTEND move
- [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ]
+ [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
+| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
+| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
+| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
END
(** Revert *)
@@ -231,15 +231,15 @@ END
(* Fix *)
TACTIC EXTEND fix
- [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
-| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+ [ "fix" natural(n) ] -> [ Tactics.fix None n ]
+| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
END
(* Cofix *)
TACTIC EXTEND cofix
- [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
-| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+ [ "cofix" ] -> [ Tactics.cofix None ]
+| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
END
(* Clear *)
@@ -247,7 +247,7 @@ END
TACTIC EXTEND clear
[ "clear" hyp_list(ids) ] -> [
if List.is_empty ids then Tactics.keep []
- else Proofview.V82.tactic (Tactics.clear ids)
+ else Tactics.clear ids
]
| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
END
@@ -261,7 +261,7 @@ END
(* Generalize dependent *)
TACTIC EXTEND generalize_dependent
- [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ]
+ [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
END
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 1f3eb13355..451e0987b0 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -582,7 +582,7 @@ END
during dependent induction. For internal use. *)
TACTIC EXTEND specialize_eqs
-[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ]
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
END
(**********************************************************************)
@@ -728,7 +728,7 @@ let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
Tacticals.New.tclTHENLIST
- [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+ [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d650cb5c6f..5d282a6936 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
- Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma)
+ Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
end }
end
| TacApply (a,ev,cb,cl) ->
@@ -1714,7 +1714,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
- let tac = Proofview.V82.tactic (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) in
+ let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
Sigma.Unsafe.of_pair (tac, sigma)
end }
end
@@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
- let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in
+ let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
Sigma.Unsafe.of_pair (tac, sigma)
end }
end
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES false
(name_atomic ~env
(TacGeneralize cl)
- (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+ (Tactics.generalize_gen cl)) sigma
end }
| TacLetTac (na,c,clp,b,eqpat) ->
Proofview.V82.nf_evar_goals <*>
@@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
Sigma.Unsafe.of_pair (c, sigma)
end } in
- Proofview.V82.tactic (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl))
+ Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end }
end
| TacChange (Some op,c,cl) ->
@@ -1889,25 +1889,22 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
- Proofview.V82.tactic begin fun gl ->
- let op = interp_typed_pattern ist env sigma op in
- let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
- let c_interp patvars = { Sigma.run = begin fun sigma ->
- let lfun' = Id.Map.fold (fun id c lfun ->
- Id.Map.add id (Value.of_constr c) lfun)
- patvars ist.lfun
- in
- let ist = { ist with lfun = lfun' } in
- try
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = interp_constr ist env sigma c in
- Sigma.Unsafe.of_pair (c, sigma)
- with e when to_catch e (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
- end } in
- (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
- gl
- end
+ let op = interp_typed_pattern ist env sigma op in
+ let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+ let c_interp patvars = { Sigma.run = begin fun sigma ->
+ let lfun' = Id.Map.fold (fun id c lfun ->
+ Id.Map.add id (Value.of_constr c) lfun)
+ patvars ist.lfun
+ in
+ let ist = { ist with lfun = lfun' } in
+ try
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = interp_constr ist env sigma c in
+ Sigma.Unsafe.of_pair (c, sigma)
+ with e when to_catch e (* Hack *) ->
+ errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ end } in
+ Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
end }
end
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 655bfd5f52..c0cae84c02 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -102,7 +102,7 @@ let assert_ ?by c =
let apply c = Tactics.apply c
-let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl)
+let clear id = Tactics.clear [id]
let assumption = Tactics.assumption
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 07:59:23 +0000