diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-18 20:29:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-18 23:26:41 +0200 |
| commit | 7d697193ab175b6bfa3c773880c0a06348449d19 (patch) | |
| tree | ea863b9f523e367add2dc832985a78ed14788fd7 /proofs/proofview.ml | |
| parent | 4a76d2034983462175219426ec47c45a3c60d4fe (diff) | |
Making Evarutil.new_evar monotonous.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f549913f2..bc2cc3e91 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -65,7 +65,9 @@ let dependent_init = let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; } | TCons (env, sigma, typ, t) -> - let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in |