Commit 736d3efb authored by Francois Bobot's avatar Francois Bobot

Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé...

Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé par la fonction retrieve.
parent a8f76c2f
......@@ -497,16 +497,17 @@ let create_env =
exception TheoryNotFound of string list * string
let find_theory env sl s =
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
try Mnm.find s m
try
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s))
let env_tag env = env.env_tag
......
......@@ -146,9 +146,12 @@ exception EmptyDecl
(** Environements *)
type retrieve_theory = env -> string list -> theory Mnm.t
(* a function of type retrieve_theory is a partial function it can
raise Not_found if it can't retrieve this theory*)
val create_env : retrieve_theory -> env
exception TheoryNotFound of string list * string
val find_theory : env -> string list -> string -> theory
......
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