Commit 02862184 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

minor change

parent 83d980f6
...@@ -906,7 +906,7 @@ let euf_auto_guard side b state sk fk = ...@@ -906,7 +906,7 @@ let euf_auto_guard side b state sk fk =
let sk' state fk = sk (simplify state) fk in let sk' state fk = sk (simplify state) fk in
(* TODO : this should be done similarly to cca_auto_guard_data! (* this should be done similarly to cca_auto_guard_data!
get the matching pairs of check(_),check(_), deduce a list of g_data, get the matching pairs of check(_),check(_), deduce a list of g_data,
apply etc ..*) apply etc ..*)
assert false assert false
...@@ -914,6 +914,7 @@ let euf_auto_guard side b state sk fk = ...@@ -914,6 +914,7 @@ let euf_auto_guard side b state sk fk =
with with
| Bad_euf s -> sk (add_error ("Bad Euf : " ^ s) state) fk | Bad_euf s -> sk (add_error ("Bad Euf : " ^ s) state) fk
(*****************) (*****************)
(* CCA Functions *) (* CCA Functions *)
(*****************) (*****************)
......
...@@ -53,20 +53,21 @@ let get_sort : type a. a term -> a sort = ...@@ -53,20 +53,21 @@ let get_sort : type a. a term -> a sort =
| EQ _ -> Bool | EQ _ -> Bool
let make : type a. a term_cnt -> a term = fun c -> let make : type a. a term_cnt -> a term = fun c ->
let c' = { hash = !hcons_cpt ; content = c } in let c' = { hash = !hcons_cpt;
content = c } in
match get_sort c' with match get_sort c' with
| Msg -> | Msg ->
begin try HT.find ht c' with begin try HT.find ht c' with
| Not_found -> | Not_found ->
incr hcons_cpt ; incr hcons_cpt;
HT.add ht c' ; HT.add ht c';
c' end c' end
| Bool -> | Bool ->
begin try HB.find hb c' with begin try HB.find hb c' with
| Not_found -> | Not_found ->
incr hcons_cpt ; incr hcons_cpt;
HB.add hb c' ; HB.add hb c';
c' end c' end
let t_hash : type a. a term -> int = fun t -> t.hash let t_hash : type a. a term -> int = fun t -> t.hash
...@@ -123,6 +124,7 @@ let t_true () = make True ...@@ -123,6 +124,7 @@ let t_true () = make True
let t_false () = make False let t_false () = make False
(****************) (****************)
(* Environement *) (* Environement *)
(****************) (****************)
...@@ -499,6 +501,7 @@ let bindings_to_print env = ...@@ -499,6 +501,7 @@ let bindings_to_print env =
StringMap.fold (fun _ b b' -> (not b) || b') StringMap.fold (fun _ b b' -> (not b) || b')
env.hide_bindings false env.hide_bindings false
(*******************) (*******************)
(* Variable typing *) (* Variable typing *)
(*******************) (*******************)
...@@ -622,7 +625,6 @@ let rec get_head env term = match term.content with ...@@ -622,7 +625,6 @@ let rec get_head env term = match term.content with
| _ -> None | _ -> None
(*****************) (*****************)
(* Miscellaneous *) (* Miscellaneous *)
(*****************) (*****************)
...@@ -697,6 +699,7 @@ let rec set_binded_names : type a. env -> a term -> a term = ...@@ -697,6 +699,7 @@ let rec set_binded_names : type a. env -> a term -> a term =
t_eq (set_binded_names env u) t_eq (set_binded_names env u)
(set_binded_names env v) (set_binded_names env v)
(*****************) (*****************)
(* Size Function *) (* Size Function *)
(*****************) (*****************)
...@@ -801,7 +804,6 @@ let env_remove_binding env s = ...@@ -801,7 +804,6 @@ let env_remove_binding env s =
hide_bindings = StringMap.remove s env.hide_bindings } hide_bindings = StringMap.remove s env.hide_bindings }
(********************) (********************)
(* Subterm Checking *) (* Subterm Checking *)
(********************) (********************)
...@@ -1141,6 +1143,7 @@ let same_elim : type a. a term -> a term = fun t -> ...@@ -1141,6 +1143,7 @@ let same_elim : type a. a term -> a term = fun t ->
aux t aux t
(***************************) (***************************)
(* Appearance Order Graphs *) (* Appearance Order Graphs *)
(***************************) (***************************)
......
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