From 4158d921d506ce931ec940c55005f0698be9616b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Oct 2014 19:30:27 +0200
Subject: Revert "Naming main goal "Main""

(More thinking needed)
---
 proofs/proofview.ml | 3 +--
 1 file changed, 1 insertion(+), 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; }
-- 
cgit v1.2.3