diff options
| author | Arnaud Spiwack | 2015-01-06 16:09:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-06 16:10:00 +0100 |
| commit | 2b00f74f104586c8d8b205161320e850efa91268 (patch) | |
| tree | 086db10b58f0cd8e6639233ef7a4cd311d988de6 | |
| parent | 91c9e77b8d75a3c04b64337805d2ce335b27c875 (diff) | |
Fix setoid rewrite.
Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].
| -rw-r--r-- | tactics/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9d9847ea57..08055004fd 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1477,7 +1477,7 @@ let assert_replacing id newt tac = else decl :: nc') env ~init:[] in - Proofview.Refine.refine begin fun sigma -> + Proofview.Refine.refine ~unsafe:false begin fun sigma -> let env' = Environ.reset_with_named_context (val_of_named_context nc') env in let sigma, ev = Evarutil.new_evar env' sigma concl in let sigma, ev' = Evarutil.new_evar env sigma newt in @@ -1507,7 +1507,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.Unsafe.tclNEWGOALS gls in + let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1521,7 +1521,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.Unsafe.tclNEWGOALS gls + Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> |