diff options
| author | filliatr | 1999-12-05 18:46:38 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-05 18:46:38 +0000 |
| commit | c70bdc0f7ddfca7055d1af4d81086485518056af (patch) | |
| tree | 081e2cb705e150d9b49b6cda91bb6e3ad58d67fa /proofs | |
| parent | e22c71e0edeccc537bb8e584812ad0646ec0dd84 (diff) | |
premier debugage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 |
3 files changed, 4 insertions, 2 deletions
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 |