diff options
Diffstat (limited to 'proofs')
| -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 03f3d906c2..d8ef207ffa 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 7dda942106..d520d200db 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 |