From 098d38249daae1ead55ccc1bf04faabcaa47d464 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Jul 2012 13:33:07 +0000
Subject: Practical fix for bug #1206 (anomaly raised in pretyping instead of
 error when called on ill-typed term, because pretyping called retyping which
 in turn is expected to be called only with typable arguments).

Incidentally, #1206 shows once more time the problem of confusion
between section variables (which morally don't have to be cleared) and
their copy in goal (which can be cleared).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15533 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 254adb5f62..e5b973d5b0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -242,9 +242,18 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let pretype_ref evdref env ref =
-  let c = constr_of_global ref in
-    make_judge c (Retyping.get_type_of env Evd.empty c)
+let pretype_ref loc evdref env = function
+  | VarRef id ->
+      (* Section variable *)
+      (try let (_,_,ty) = lookup_named id env in make_judge (mkVar id) ty
+       with Not_found ->
+         (* This may happen if env is a goal env and section variables have
+            been cleared - section variables should be different from goal
+            variables *)
+         Pretype_errors.error_var_not_found_loc loc id)
+  | ref ->
+      let c = constr_of_global ref in
+      make_judge c (Retyping.get_type_of env Evd.empty c)
 
 let pretype_sort evdref = function
   | GProp -> judge_of_prop
@@ -262,7 +271,7 @@ let new_type_evar evdref env loc =
 let rec pretype (tycon : type_constraint) env evdref lvar = function
   | GRef (loc,ref) ->
       inh_conv_coerce_to_tycon loc env evdref
-	(pretype_ref evdref env ref)
+	(pretype_ref loc evdref env ref)
 	tycon
 
   | GVar (loc, id) ->
-- 
cgit v1.2.3