diff options
| author | Hugo Herbelin | 2014-10-16 19:30:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-16 22:28:35 +0200 |
| commit | 4158d921d506ce931ec940c55005f0698be9616b (patch) | |
| tree | d7025e8bebddb0fe7308194ffeecd1940b362f30 | |
| parent | d0da8a75cd1d600afa68da5e995d39a415234c2d (diff) | |
Revert "Naming main goal "Main""
(More thinking needed)
| -rw-r--r-- | proofs/proofview.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 34d53c3f21..d7f79f46fb 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -116,8 +116,7 @@ let init sigma = | (env, typ) :: l -> let ret, { solution = sol; comb = comb } = aux l in let src = (Loc.ghost,Evar_kinds.GoalEvar) 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 (new_defs , econstr) = Evarutil.new_evar env sol ~src typ in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in entry, { solution = new_defs; comb = gl::comb; } |
