diff options
| author | Pierre-Marie Pédrot | 2018-12-16 13:54:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-16 13:54:40 +0100 |
| commit | 7e155688331c8f004f34950da67108d7284e4e56 (patch) | |
| tree | 9182191cd348bc32eaa8cdd00b615a924ed17c6f /plugins/ltac/rewrite.ml | |
| parent | 2a7992f75c86a15512568ac61ca4c43e23242b28 (diff) | |
| parent | a2549c7f716e870ea19fdbfd7b5493117fe21e76 (diff) | |
Merge PR #9172: [proof] Rework proof interface.
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e626df5579..4bb52f599a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -632,7 +632,8 @@ let solve_remaining_by env sigma holes by = | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in + let name, poly = Id.of_string "rewrite", false in + let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep |