diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-06 14:51:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-06 14:51:12 +0200 |
| commit | 9bc1ddceda626730318798e58e7f309e4a334053 (patch) | |
| tree | 382b102c374e527d14cefbe8fcada5dabc7b8d67 /proofs/refine.ml | |
| parent | bb5fa2a3a2a1e398683d38a8731faa2ff3ec39b0 (diff) | |
Fix a refine anomaly "Evar defined twice".
Because the argument given to refine may mess with the evarmap, the goal being
refined can be solved by side-effect after the term filler is computed. If this
happens, we simply don't perform the refining operation.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 4161d7104..e3f650848 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -102,7 +102,12 @@ let generic_refine ~typecheck f gl = in (** Proceed to the refinement *) let c = EConstr.Unsafe.to_constr c in - let sigma = match evkmain with + let sigma = match Proofview.Unsafe.advance sigma self with + | None -> + (** Nothing to do, the goal has been solved by side-effect *) + sigma + | Some self -> + match evkmain with | None -> Evd.define self c sigma | Some evk -> let id = Evd.evar_ident self sigma in |