diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-29 15:20:33 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-29 15:20:33 +0000 |
commit | d204288bf38e3cecc2a60f07ce0b1bc3681f56da (patch) | |
tree | 0e7d9c6463083fc14819061a908c5536e795ecce | |
parent | 29c33c1143635d89b82048835082c133439fffbd (diff) |
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
-rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 7 |
3 files changed, 10 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index bb1bfb67e..bd65b6ab2 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 4747bf065..812f3e934 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 f8fcc9b9e..1ca81e8c4 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' |