From f0a793f123683eaab6bab9968725febe7c311f05 Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 31 Oct 2000 13:57:01 +0000 Subject: - simplification Makefile (compilation des fichiers .ml'; pas encore parfait car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7b7c95d4bf..af46e221e2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -208,7 +208,8 @@ let unsafe_infer_type env constr = (* ``Type of'' machines. *) let type_of env c = - let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) + let (j,_) = safe_infer env c in + nf_betaiota env Evd.empty (body_of_type j.uj_type) (* Typing of several terms. *) @@ -281,12 +282,15 @@ let add_constant_with_value sp body typ env = let (jt,cst') = safe_infer env ty in let env'' = add_constraints cst' env' in try - let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in + let cst'' = + conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val + in let env'' = add_constraints cst'' env'' in (env'', assumption_of_judgment env'' Evd.empty jt, Constraint.union cst' cst'') with NotConvertible -> - error_actual_type CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val + error_actual_type + CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val in let ids = Idset.union (global_vars_set body) (global_vars_set (body_of_type ty)) @@ -396,7 +400,8 @@ let type_one_constructor env_ar nparams arsort c = let infos = let (params,dc) = mind_extract_params nparams c in let env_par = push_rels params env_ar in - infos_and_sort env_par dc in + infos_and_sort env_par dc + in (* Constructors are typed-checked here *) let (j,cst) = safe_infer_type env_ar c in -- cgit v1.2.3