Skip to content
Snippets Groups Projects
Commit cb20ed6b authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[qed] Subst.find is better

parent 5ce723d9
No related branches found
No related tags found
No related merge requests found
......@@ -334,7 +334,7 @@ sig
val create : ?pool:pool -> unit -> t
val fresh : t -> tau -> var
val get : t -> term -> term
val find : t -> term -> term
val filter : t -> term -> bool
val add : t -> term -> term -> unit
......
......@@ -2251,7 +2251,7 @@ struct
| FUN(f,s) -> (try call f e with Not_found -> compute e s)
| MAP(m,s) -> (try Tmap.find e m with Not_found -> compute e s)
let get sigma a = compute a sigma.shared
let find sigma a = compute a sigma.shared
let filter sigma a =
List.for_all (fun f -> f a) sigma.filter
......@@ -2302,7 +2302,7 @@ struct
else e
and compute mu sigma alpha e =
try Subst.get sigma e with Not_found ->
try Subst.find sigma e with Not_found ->
let r =
match e.repr with
| Bvar(k,_) -> Intmap.find k alpha
......
......@@ -376,7 +376,7 @@ sig
module Subst :
sig
val get : sigma -> term -> term
val find : sigma -> term -> term
val add : sigma -> term -> term -> unit
val add_map : sigma -> term Tmap.t -> unit
val add_fun : sigma -> (term -> term) -> unit
......
......@@ -311,7 +311,7 @@ struct
}
let mem_lit l sigma =
try F.Subst.get (subst sigma) l == e_true
try F.Subst.find (subst sigma) l == e_true
with Not_found -> false
let add_lit l sigma =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment