diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 630f64f7b5..6a574a56e2 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -392,7 +392,7 @@ let interp_prim_token = let interp_prim_token_cases_pattern_expr loc looked_for p = interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p -let rec interp_notation loc ntn local_scopes = +let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try find_interpretation ntn (find_notation ntn) scopes with Not_found -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ad1bd11381..ae851d8ba3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -110,7 +110,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x) -let rec glob_constr_of_notation_constr loc x = +let glob_constr_of_notation_constr loc x = let rec aux () x = glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x @@ -544,7 +544,7 @@ let rec match_iterated_binders islambda decls = function let remove_sigma x (sigmavar,sigmalist,sigmabinders) = (List.remove_assoc x sigmavar,sigmalist,sigmabinders) -let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin = +let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in |