Suppression des local_constraints, des ctxtty et du focus.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5d015dbf8..f6424df8d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -204,7 +204,7 @@ let delete_all_proofs = init_proofs
 (*********************************************************************)
 
 let start_proof na str sign concl =
-  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
+  let top_goal = mk_goal sign concl in
   let ts = { 
     top_hyps = (sign,empty_named_context);
     top_goal = top_goal;