diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/dp/dp_why.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/dp/dp_why.ml')
-rw-r--r-- | contrib/dp/dp_why.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml index e1ddb039..e24049ad 100644 --- a/contrib/dp/dp_why.ml +++ b/contrib/dp/dp_why.ml @@ -4,6 +4,18 @@ open Format open Fol +type proof = + | Immediate of Term.constr + | Fun_def of string * (string * typ) list * typ * term + +let proofs = Hashtbl.create 97 +let proof_name = + let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r + +let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n + +let find_proof = Hashtbl.find proofs + let rec print_list sep print fmt = function | [] -> () | [x] -> print fmt x |