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

1 files changed, 8 insertions, 1 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0494d44e5..81bd6987f 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