diff options
| author | Maxime Dénès | 2017-09-11 10:49:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-11 10:49:22 +0200 |
| commit | e22809bbe533f9dc0c36146b44ae3e6f9513cd32 (patch) | |
| tree | 0303f803d37350954f32dcc6f7282347f3a9951e | |
| parent | d4a8aa6339836b8ae1f37ae7ff67757009683542 (diff) | |
| parent | 9bc1ddceda626730318798e58e7f309e4a334053 (diff) | |
Merge PR #1029: Fix a refine anomaly "Evar defined twice".
| -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 4161d71047..e3f6508481 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 |