From f64a0c8a627ae9026dfb20ffec5f8906f4c9b578 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Sun, 17 Jan 2016 14:27:35 +0100 Subject: [PATCH] Detect_polymorphism: minor --- src/transform/detect_polymorphism.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/transform/detect_polymorphism.ml b/src/transform/detect_polymorphism.ml index 9e6e11f3f..9be5fca15 100644 --- a/src/transform/detect_polymorphism.ml +++ b/src/transform/detect_polymorphism.ml @@ -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@." -- GitLab