diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0428f08138..f5098d2a34 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -348,6 +349,7 @@ let constr_flags () = { Pretyping.fail_evar = false; Pretyping.expand_evars = true; Pretyping.program_mode = false; + Pretyping.polymorphic = false; } let refine_tac ist simple with_classes c = @@ -813,9 +815,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; } END (* ********************************************************************* *) @@ -913,9 +915,9 @@ END the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -| [ "Grab" "Existential" "Variables" ] +| ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } END (* Shelves all the goals under focus. *) @@ -945,9 +947,9 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve -| [ "Unshelve" ] +| ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1098,8 +1100,8 @@ END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { Proof_global.compact_the_proof () } +| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> + { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END |