diff options
| author | herbelin | 2004-02-03 17:32:58 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-03 17:32:58 +0000 |
| commit | ad6aa3994f75a94580bcea1bb77c5b6808bd5e39 (patch) | |
| tree | e706ce8b31ff3193b866a2ab07a7061fcd560b4c | |
| parent | b9084e97bc18bf65195779c44f496901bb83e009 (diff) | |
Backtrack sur recuperation de noms a partir du type, car casse la correction des dependances de nom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ca81e8c4e..56cb747b64 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -154,10 +154,6 @@ 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)) @@ -321,7 +317,6 @@ let rec pretype tycon env isevars lvar = function 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' |