diff options
| author | Pierre-Marie Pédrot | 2015-11-15 13:30:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-15 13:30:41 +0100 |
| commit | 7e7749ed22c328e041eb8ab59df5b6d32f777653 (patch) | |
| tree | bf4338e577fd43d1fb6985691226784e0ce57e1b /tactics | |
| parent | f0ff590f380fb3d9fac6ebfdd6cfd7bf6874658e (diff) | |
| parent | 3aeb18bf1412a27309c39713e05eca2c27706ca8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d1b14e3d99..9a19d4bda7 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1509,7 +1509,7 @@ let assert_replacing id newt tac = let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in let nc = match before with | [] -> assert false - | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem + | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Proofview.Refine.refine ~unsafe:false { run = begin fun sigma -> @@ -2081,8 +2081,10 @@ let poly_proof getp gett env evm car rel = let setoid_reflexivity = setoid_proof "reflexive" (fun env evm car rel -> - tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof - env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c))) + tac_open (poly_proof PropGlobal.get_reflexive_proof + TypeGlobal.get_reflexive_proof + env evm car rel) + (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c)))) (reflexivity_red true) let setoid_symmetry = |