blob: b60a27e6319a5d76ca884a4164bc760ad8829e03 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
open Util
open Pp
open Term
open Tacmach
open Fol
let simplify gl =
let concl = pf_concl gl in
if not (is_Prop (pf_type_of gl concl)) then error "not a proposition";
msgnl (str "nb of hyps = " ++ int (List.length (pf_hyps gl)));
pp_flush ();
error "not yet implemented"
|
