diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bc251d33de..7eb32f34a2 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -31,10 +31,10 @@ let proofview p = (* Initialises a proofview, the argument is a list of environement, conclusion types, and optional names, creating that many initial goals. *) -let init = +let init sigma = let rec aux = function | [] -> { initial = [] ; - solution = Evd.empty ; + solution = sigma ; comb = []; } | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } = |