Commit f64a0c8a authored by Andrei Paskevich's avatar Andrei Paskevich

Detect_polymorphism: minor

parent 1fd7832d
......@@ -13,11 +13,12 @@ open Decl
open Theory
let debug = Debug.register_info_flag "detect_poly"
~desc:"Print@ debugging@ messages@ of@ the@ 'detect_polymorphism'@ transformation."
~desc:"Print@ debugging@ messages@ of@ the@ \
'detect_polymorphism'@ transformation."
(* metas to attach to symbols or propositions to tell their polymorphic
nature can be ignored because it will be treated specifically by
drivers *)
nature can be ignored because it will be treated specifically by
drivers *)
let meta_ignore_polymorphism_ts =
register_meta
......@@ -50,7 +51,7 @@ let check_ls ign_ls ls =
List.fold_left
(fun acc ty -> acc || not (Ty.ty_closed ty))
false
(Opt.fold (fun acc x -> x :: acc) ls.Term.ls_args ls.Term.ls_value)
(Ty.oty_cons ls.Term.ls_args ls.Term.ls_value)
let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
Debug.dprintf debug "[detect_polymorphism] |sts|=%d |sls|=%d |spr|=%d@."
......
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