diff options
| author | Hugo Herbelin | 2014-08-21 12:39:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:32 +0200 |
| commit | 32e2b1ba856f330dae03fbbf16365a08c2cc2f20 (patch) | |
| tree | 4c05fb027aef0649eccadb81f5bea16b4ba7c5b6 /proofs | |
| parent | 19adfa9994e4772a7f039f2c3880e5d26dd45b12 (diff) | |
Fix source of initial goal.
Diffstat (limited to 'proofs')
| -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 98be5a5d5b..661b32601c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -39,7 +39,8 @@ let init sigma = | [] -> [], { solution = sigma; comb = []; } | (env, typ) :: l -> let ret, { solution = sol; comb = comb } = aux l in - let (new_defs , econstr) = Evarutil.new_evar sol env typ in + let src = (Loc.ghost,Evar_kinds.GoalEvar) in + let (new_defs , econstr) = Evarutil.new_evar sol env ~src typ in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in let entry = (econstr, typ) :: ret in |