diff options
| author | Maxime Dénès | 2018-02-19 11:12:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-19 11:12:52 +0100 |
| commit | eaff61e0a19fcf6ebc2a9a8ae17327413274c67b (patch) | |
| tree | acbbc416ad78bf8520893405c04855c600909576 /grammar | |
| parent | 073b92396a68be30f77c80960a58ca562bb01f49 (diff) | |
| parent | 68935660fbfdec2e357e123ed999073ed3b8fc26 (diff) | |
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.mlp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 9742a002d7..01138702bc 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -138,7 +138,6 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = <:expr< let f = $lid:f$ in fun ist v -> Ftactic.enter (fun gl -> - let gl = Proofview.Goal.assume gl in let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) |