From d204288bf38e3cecc2a60f07ce0b1bc3681f56da Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 29 Jan 2004 15:20:33 +0000
Subject: Reparation d'une rupture (en presence de types implicites) de
 l'invariant que les variables liees sont toujours nommees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml  | 6 +++---
 pretyping/evarutil.mli | 2 +-
 pretyping/pretyping.ml | 7 ++++++-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index bb1bfb67e1..bd65b6ab27 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -564,15 +564,15 @@ let define_evar_as_sort isevars (ev,args) =
    an evar instantiate it with the product of 2 new evars. *)
 
 let split_tycon loc env isevars = function
-  | None -> None,None
+  | None -> Anonymous,None,None
   | Some c ->
       let sigma = evars_of isevars in
       let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-        | Prod (na,dom,rng) -> Some dom, Some rng
+        | Prod (na,dom,rng) -> na, Some dom, Some rng
 	| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
 	    let (_,evdom,evrng) = refine_evar_as_arrow isevars ev in
-	    Some (mkEvar evdom), Some (mkEvar evrng)
+	    Anonymous, Some (mkEvar evdom), Some (mkEvar evrng)
 	| _ -> error_not_product_loc loc env sigma c
 
 let valcon_of_tycon x = x
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4747bf065e..812f3e9342 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -89,7 +89,7 @@ val mk_valcon : constr -> val_constraint
 
 val split_tycon :
   Rawterm.loc -> env ->  evar_defs -> type_constraint -> 
-    type_constraint * type_constraint
+    name * type_constraint * type_constraint
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f8fcc9b9ed..1ca81e8c4e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -154,6 +154,10 @@ let evar_type_case isevars env ct pt lft p c =
   in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
 *)
 
+let adjust_name_from_type name = function
+  | Anonymous -> name
+  | na -> na
+
 let strip_meta id = (* For Grammar v7 compatibility *)
   let s = string_of_id id in
   if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
@@ -314,9 +318,10 @@ let rec pretype tycon env isevars lvar = function
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 
   | RLambda(loc,name,c1,c2)      ->
-      let (dom,rng) = split_tycon loc env isevars tycon in
+      let (name',dom,rng) = split_tycon loc env isevars tycon in
       let dom_valcon = valcon_of_tycon dom in
       let j = pretype_type dom_valcon env isevars lvar c1 in
+      let name = adjust_name_from_type name' name 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'
-- 
cgit v1.2.3