From 73cdb000ec07ec484557839c4b94fcf779df2f06 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 May 2016 00:16:09 +0200 Subject: Put the "clear" tactic into the monad. --- ltac/coretactics.ml4 | 2 +- ltac/tauto.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 8b5f527cd0..4e2dfafb52 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -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 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 -- cgit v1.2.3 From 12f4c8ed277fa8368cab2e99f173339a64bcef3d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 18:34:21 +0200 Subject: Put the "fix" tactic in the monad. --- ltac/coretactics.ml4 | 4 ++-- ltac/tacinterp.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 4e2dfafb52..98b77ab357 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -231,8 +231,8 @@ 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 *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d650cb5c6f..5e0153fcee 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -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 -- cgit v1.2.3 From 9ae9ac00b6882a9918eea3cb7d809424695d37ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 20:57:34 +0200 Subject: Put the "exact" family of tactic in the monad. --- ltac/coretactics.ml4 | 2 +- ltac/tacinterp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 98b77ab357..3849a84405 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -39,7 +39,7 @@ 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 diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5e0153fcee..7acdff9acf 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"") 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) -> -- cgit v1.2.3 From 1394bab8ba40dd4714e941586109fd88a79ef653 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:14:12 +0200 Subject: Put the "*_cast_no_check" tactics in the monad. --- ltac/coretactics.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 3849a84405..4893e40973 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -43,11 +43,11 @@ TACTIC EXTEND exact_no_check 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 -- cgit v1.2.3 From a4bd166bd2119a5290276f0ded44f8186ba1ecee Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:21:42 +0200 Subject: Put the "cofix" tactic in the monad. --- ltac/coretactics.ml4 | 4 ++-- ltac/tacinterp.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 4893e40973..766f0714d2 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -238,8 +238,8 @@ 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 *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 7acdff9acf..5aff262aa5 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -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 -- cgit v1.2.3 From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:41:55 +0200 Subject: Put the "generalize" tactic in the monad. --- ltac/extratactics.ml4 | 2 +- ltac/tacinterp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 1f3eb13355..e03cc675e7 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -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 5aff262aa5..7ec1b2ca0c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -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 <*> -- cgit v1.2.3 From c6a16e8cc607f70f519f3ebbd5856b8ff501d782 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:18:12 +0200 Subject: Put the "generalize dependent" tactic in the monad. --- ltac/coretactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 766f0714d2..b7fc63cd56 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -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.) *) -- cgit v1.2.3 From fd5898afa9a89ca61f87cdeca4ae982a024e4d4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:24:45 +0200 Subject: Put the "specialize_eq" tactic in the monad. --- ltac/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e03cc675e7..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 (**********************************************************************) -- cgit v1.2.3 From ed1c4d01388bf11710b38f1c302d405233c24647 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:58:07 +0200 Subject: Put the "change" tactic in the monad. --- ltac/tacinterp.ml | 37 +++++++++++++++++-------------------- 1 file changed, 17 insertions(+), 20 deletions(-) (limited to 'ltac') diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 7ec1b2ca0c..5d282a6936 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -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 -- cgit v1.2.3 From cddddce068bc0482f62ffab8e412732a307b90bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 May 2016 10:47:53 +0200 Subject: Put the "move" tactic in the monad. --- ltac/coretactics.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index b7fc63cd56..ce28eacc09 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -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 *) -- cgit v1.2.3