diff options
| author | Hugo Herbelin | 2014-10-01 09:44:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-13 19:12:34 +0200 |
| commit | 51934650858ad04c6fff2ffe2d017b7a1a20bd1c (patch) | |
| tree | 22139e0c77649352ddc4efda7a65a3337c7d2ace | |
| parent | 56cb514b425360ca428be116e9ea1d5205edd06f (diff) | |
Naming main goal "Main"
| -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 c8f1921c10..04c084fb77 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -40,7 +40,8 @@ let init sigma = | (env, typ) :: l -> let ret, { solution = sol; comb = comb } = aux l in let src = (Loc.ghost,Evar_kinds.GoalEvar) in - let (new_defs , econstr) = Evarutil.new_evar env sol ~src typ in + let naming = Misctypes.IntroIdentifier (Names.Id.of_string "Main") in + let (new_defs , econstr) = Evarutil.new_evar env sol ~src ~naming typ in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in let entry = (econstr, typ) :: ret in |