diff options
| author | Arnaud Spiwack | 2014-10-21 21:53:35 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:45 +0200 |
| commit | a5a355ec3e9cbbfa28be53b9ba6ef914136b0aba (patch) | |
| tree | 7d005f87c55567d8a120b7cdc4679fad04810e5c /tactics | |
| parent | cadfe23210c8edaab1f22d0edb7acc33fb9ff782 (diff) | |
Proofview: move more functions to the Unsafe module.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index ec9a9ff3e7..1e3996429b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1477,7 +1477,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match is_hyp, prf with | Some id, Some p -> - let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.tclNEWGOALS gls in + let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1491,7 +1491,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let (sigma, ev) = Evarutil.new_evar env sigma newt in sigma, mkApp (p, [| ev |]) in - Proofview.Refine.refine make <*> Proofview.tclNEWGOALS gls + Proofview.Refine.refine make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> |