diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:12:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:28:52 +0200 |
| commit | 2d747797c427818cdf85d0a0d701c7c9b0106b82 (patch) | |
| tree | fe2a13b39348723dc7a4567198da190650cce2d4 /proofs/proofview.ml | |
| parent | 4cc1714ac9b0944b6203c23af8c46145e7239ad3 (diff) | |
Proofview.Goal.sigma returns an indexed evarmap.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 826b4772a..bded518e7 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -921,7 +921,7 @@ module Goal = struct let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) let env { env=env } = env - let sigma { sigma=sigma } = sigma + let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma let hyps { env=env } = Environ.named_context env let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self @@ -1061,6 +1061,7 @@ struct let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> let sigma = Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Goal.env gl in let concl = Goal.concl gl in (** Save the [future_goals] state to restore them after the |