Code mort

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

1 files changed, 0 insertions, 28 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index df0c493d5..7ac4c07b0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -58,24 +58,6 @@ let get_state () =
 let get_topstate ()    = snd(get_state())
 let get_pftreestate () = fst(get_state())
 
-(*i
-let get_evmap_sign og =
-  let og = match og with
-    | Some n ->
-        let pftree = get_pftreestate () in
-        Some (nth_goal_of_pftreestate n pftree)
-    | None ->
-        try
-          let pftree = get_pftreestate () in
-          Some (nth_goal_of_pftreestate 1 pftree)
-        with e when Logic.catchable_exception e -> 
-	  None 
-  in
-  match og with
-    | Some goal -> (project goal, pf_env goal)
-    | _ -> (Evd.empty, Global.env())
-i*)
-
 let get_goal_context n =
   let pftree = get_pftreestate () in
   let goal = nth_goal_of_pftreestate n pftree in
@@ -221,16 +203,6 @@ let start_proof na str sign concl =
   start(na,ts);
   set_current_proof na
 
-(*
-let start_proof_constr na str concl =
-  let sigma = Evd.empty in
-  let env = Global.env() in
-(* Si c'est un constr, il est supposé typable dans le contexte courant
-  let _ = execute_type env sigma concl in
-*)
-  start_proof_with_type na str env concl
-*)
-
 let solve_nth k tac =
   let pft = get_pftreestate() in
   if not (List.mem (-1) (cursor_of_pftreestate pft)) then