Commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@372 85f007b7-540e-0410-9357-904b9bb8a0f7

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)