diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0f0907786e..9fc5265e91 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -50,13 +50,17 @@ let rec execute mf env cstr = | IsVar id -> (make_judge cstr (snd (lookup_var id env)), cst0) - + | IsAbst _ -> if evaluable_abst env cstr then execute mf env (abst_value env cstr) else error "Cannot typecheck an unevaluable abstraction" - + + (* ATTENTION : faudra faire le typage du contexte des Const, + MutInd et MutConstructsi un jour cela devient des constructions + arbitraires et non plus des variables *) + | IsConst c -> (make_judge cstr (type_of_constant env Evd.empty c), cst0) |