diff options
Diffstat (limited to 'checker/validate.ml')
| -rw-r--r-- | checker/validate.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/checker/validate.ml b/checker/validate.ml index c434ef09..f831875d 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This module defines validation functions to ensure an imported @@ -49,8 +51,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx exception ValidObjError of string * error_context * Obj.t let fail ctx o s = raise (ValidObjError(s,ctx,o)) -type func = error_context -> Obj.t -> unit - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () |