aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-16 19:30:27 +0200
committerHugo Herbelin2014-10-16 22:28:35 +0200
commit4158d921d506ce931ec940c55005f0698be9616b (patch)
treed7025e8bebddb0fe7308194ffeecd1940b362f30
parentd0da8a75cd1d600afa68da5e995d39a415234c2d (diff)
Revert "Naming main goal "Main""
(More thinking needed)
-rw-r--r--proofs/proofview.ml3
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; }