From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- plugins/funind/glob_termops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/glob_termops.ml') diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 01e5ef7fb..4e561fc7e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -406,7 +406,7 @@ let is_free_in id = | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> false | GHole _ -> false | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -502,7 +502,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -655,7 +655,7 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> -- cgit v1.2.3