diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 10 |
3 files changed, 12 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 5b6064fa9f..13761ca245 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -44,6 +44,10 @@ struct | None -> true | Some _ -> false + let is_valid_ident_part s = match Unicode.ident_refutation ("x"^s) with + | None -> true + | Some _ -> false + let of_bytes s = let s = Bytes.to_string s in check_valid s; diff --git a/kernel/names.mli b/kernel/names.mli index 9a4ceef802..74a4e6f7d0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -44,6 +44,9 @@ sig val is_valid : string -> bool (** Check that a string may be converted to an identifier. *) + val is_valid_ident_part : string -> bool + (** Check that a string is a valid part of an identifier *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bf02ceb2c2..6abd283f6c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -671,7 +671,7 @@ let inline_side_effects env body side_eff = let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) - if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) + if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs, 0) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in @@ -725,10 +725,10 @@ let inline_side_effects env body side_eff = else mkLetIn (na, b, ty, accu) in let body = List.fold_right fold_arg args body in - (body, ctx, sigs) + (body, ctx, sigs, len - 1) let inline_private_constants env ((body, ctx), side_eff) = - let body, ctx',_ = inline_side_effects env body side_eff in + let body, ctx', _, _ = inline_side_effects env body side_eff in let ctx' = Univ.ContextSet.union ctx ctx' in (body, ctx') @@ -880,11 +880,11 @@ let add_constant l decl senv = match decl with | OpaqueEntry ce -> let handle env body eff = - let body, uctx, signatures = inline_side_effects env body eff in + let body, uctx, signatures, skip = inline_side_effects env body eff in let trusted = check_signatures senv signatures in let trusted, uctx = match trusted with | None -> 0, uctx - | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx + | Some univs -> skip, Univ.ContextSet.union univs uctx in body, uctx, trusted in |