Commit bac4d8d1 authored by Andrei Paskevich's avatar Andrei Paskevich

remove print_theorynotfound from Env. Why was it there?

parent b6867842
...@@ -63,5 +63,3 @@ let find_theory env sl s = ...@@ -63,5 +63,3 @@ let find_theory env sl s =
let env_tag env = env.env_tag let env_tag env = env.env_tag
let print_theorynotfound fmt (l,s) =
Format.fprintf fmt "%s.%s" (String.concat "." l) s
...@@ -34,4 +34,3 @@ val env_tag : env -> int ...@@ -34,4 +34,3 @@ val env_tag : env -> int
exception TheoryNotFound of string list * string exception TheoryNotFound of string list * string
val print_theorynotfound : Format.formatter -> string list * string -> unit
...@@ -227,8 +227,9 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} = ...@@ -227,8 +227,9 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in let id,qfile = qualid_to_slist qualid in
let th = try let th = try
find_theory env qfile id find_theory env qfile id
with Env.TheoryNotFound (l,s) -> errorm ~loc "theory %a not found" with Env.TheoryNotFound (l,s) ->
Env.print_theorynotfound (l,s) in errorm ~loc "theory %s.%s not found" (String.concat "." l) s
in
let add_htheory cloned id t = let add_htheory cloned id t =
try try
let t2,t3 = Hid.find driver.drv_theory id in let t2,t3 = Hid.find driver.drv_theory id in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment