diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 942527167..a0eb9e2b2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -44,7 +44,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; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates - | Anonymous -> anomaly (Pp.str "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 = @@ -399,7 +399,7 @@ let get_funs_constant mp dp = let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly (Pp.str "Anonymous fix") + anomaly (Pp.str "Anonymous fix.") ) na | _ -> [|const,0|] |