From d5445c2068065fe3cb227c1b335118ae4196bbbf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 29 Dec 2006 17:02:04 +0000
Subject: Protection contre une source possible de liaison de lambda anonyme
 (utilisation du nom de la contrainte de type)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9468 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0494d44e58..81bd6987fe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -196,6 +196,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let push_rels vars env = List.fold_right push_rel vars env
 
+  (* used to enforce a name in Lambda when the type constraints itself
+     is named, hence possibly dependent *)
+
+  let orelse_name name name' = match name with
+    | Anonymous -> name'
+    | _ -> name
+
   (*
     let evar_type_case isevars env ct pt lft p c =
     let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
@@ -409,7 +416,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j = pretype_type dom_valcon env isevars lvar c1 in
 	let var = (name,None,j.utj_val) in
 	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-	  judge_of_abstraction env name j j'
+	  judge_of_abstraction env (orelse_name name name') j j'
 
     | RProd(loc,name,c1,c2)        ->
 	let j = pretype_type empty_valcon env isevars lvar c1 in
-- 
cgit v1.2.3