From c70bdc0f7ddfca7055d1af4d81086485518056af Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sun, 5 Dec 1999 18:46:38 +0000
Subject: premier debugage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml   | 2 +-
 proofs/pfedit.ml  | 2 +-
 proofs/pfedit.mli | 2 ++
 3 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0131df8b94..c53c462332 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -881,7 +881,7 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
-  failwith "TODO"
+  failwith "clenv_type_of: TODO"
   (***
   (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
      (gLOB(w_hyps ce.hook)) c).uj_type
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9fc3768552..6e6114f901 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -228,7 +228,7 @@ let abort_refine f x =
   f x
   (* used to be: error "Must save or abort current goal first" *)
 
-let reset_name = abort_refine reset_to
+let reset_name = abort_refine reset_name
 (*** TODO 
 and reset_keeping_name = abort_refine reset_keeping
 and reset_section = abort_refine raw_reset_section
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 966630eae4..9a528f5551 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Pp
+open Names
 open Term
 open Sign
 open Environ
@@ -50,6 +51,7 @@ val proof_term : unit -> constr
 
 val start_proof : string -> strength -> Coqast.t -> unit
 val start_proof_constr : string -> strength -> constr -> unit
+val reset_name : identifier -> unit
 
 val save_named : bool -> unit
 val save_anonymous : bool -> string -> 'a -> unit
-- 
cgit v1.2.3