diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-20 14:32:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-20 14:32:48 +0000 |
| commit | 2ba5fc92551cfe9632ad01a5ae52aa7c7d0241f6 (patch) | |
| tree | bb220c3c1a120fd1903a783de7c65cdf2cc7c952 | |
| parent | 3deb712f62aa532b3edc6d61d6af0e3f1a1b1d41 (diff) | |
Cosmétique avant tout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2209 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/tacmach.ml | 3 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 12 |
2 files changed, 7 insertions, 8 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 03f3d906c..d8ef207ff 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -112,8 +112,7 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) -let pf_check_type gls c1 c2 = - let casted = mkCast (c1, c2) in pf_type_of gls casted +let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2))) (************************************) (* Tactics handling a list of goals *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7dda94210..d520d200d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -37,23 +37,23 @@ val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c -val pf_concl : goal sigma -> constr +val pf_concl : goal sigma -> types val pf_env : goal sigma -> env val pf_hyps : goal sigma -> named_context (*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*) -val pf_hyps_types : goal sigma -> (identifier * constr) list +val pf_hyps_types : goal sigma -> (identifier * types) list val pf_nth_hyp_id : goal sigma -> int -> identifier val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> identifier list val pf_global : goal sigma -> identifier -> constr val pf_parse_const : goal sigma -> string -> constr -val pf_type_of : goal sigma -> constr -> constr -val pf_check_type : goal sigma -> constr -> constr -> constr +val pf_type_of : goal sigma -> constr -> types +val pf_check_type : goal sigma -> constr -> types -> unit val pf_execute : goal sigma -> constr -> unsafe_judgment -val hnf_type_of : goal sigma -> constr -> constr +val hnf_type_of : goal sigma -> constr -> types val pf_interp_constr : goal sigma -> Coqast.t -> constr -val pf_interp_type : goal sigma -> Coqast.t -> constr +val pf_interp_type : goal sigma -> Coqast.t -> types val pf_get_hyp : goal sigma -> identifier -> named_declaration val pf_get_hyp_typ : goal sigma -> identifier -> types |