diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 700beaff5..9916ed95a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -48,7 +48,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; (Name id,v,t)::(change_predicates_names (id::avoid) predicates) - | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " + | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ") in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -395,7 +395,7 @@ let get_funs_constant mp dp = let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly "Anonymous fix" + anomaly (Pp.str "Anonymous fix") ) na | _ -> [|const,0|] @@ -505,7 +505,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes - | _ -> anomaly "" + | _ -> anomaly (Pp.str "") in let (_,(const,_,_)) = try |