diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 6 | ||||
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 |
3 files changed, 8 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5f96e3fd6..b651053dba 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,7 +274,7 @@ let drop_implicits_in_patt cst nb_expl args = |None -> aux t |x -> x in - if nb_expl = 0 then aux impl_data + if Int.equal nb_expl 0 then aux impl_data else let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) @@ -712,7 +712,7 @@ let rec extern inctx scopes vars r = let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in let rec cut args n = - if n = 0 then args + if Int.equal n 0 then args else match args with | [] -> raise No_match @@ -907,7 +907,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if n = 0 then f else GApp (Loc.ghost,f,args1)), + (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)), args2, subscopes, impls | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c204db0e01..a6b207c1da 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -199,7 +199,7 @@ and spaces ntn n = let expand_notation_string ntn n = let pos = List.nth (wildcards ntn 0) n in - let hd = if pos = 0 then "" else String.sub ntn 0 pos in + let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in let tl = if pos = String.length ntn then "" else String.sub ntn (pos+1) (String.length ntn - pos -1) in @@ -737,7 +737,7 @@ let find_remaining_scopes pl1 pl2 ref = let impls_st = implicits_of_global ref in let len_pl1 = List.length pl1 in let len_pl2 = List.length pl2 in - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size len_pl2 impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let allscs = find_arguments_scope ref in @@ -797,7 +797,7 @@ let check_constructor_length env loc cstr len_pl pl0 = (nargs - (Inductiveops.inductive_nparams (fst cstr)))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c5cc1438b8..d3c55c1f58 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -754,7 +754,7 @@ let rec match_cases_pattern metas sigma a1 a2 = when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then raise No_match else @@ -777,7 +777,7 @@ let match_ind_pattern metas sigma ind pats a2 = | NApp (NRef (IndRef r2),l2) when ind = r2 -> let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats then raise No_match else |