diff options
| author | herbelin | 2006-12-12 10:34:05 +0000 |
|---|---|---|
| committer | herbelin | 2006-12-12 10:34:05 +0000 |
| commit | e9d9c0e5394de0fc831f392bb64908a5724e688d (patch) | |
| tree | f5c191be528b62fdef1094c6df6f6dd37b0d1de5 /pretyping | |
| parent | c278a2c2456538f47d64613068720fc9a5bdbe21 (diff) | |
Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case15.v et CasesDep.v pas anormal)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 53c6199127..207ad88b37 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -168,15 +168,20 @@ let push_rel_context_to_named_context env typ = fold_named_context (fun env (id,b,_) l -> mkVar id :: l) env ~init:[] in (* move the rel context to a named context and extend the instance with vars of the rel context *) +(* let fv = free_rels typ in +*) let avoid = ids_of_named_context (named_context env) in let n = rel_context_length (rel_context env) in let (subst, _, _, inst, env) = Sign.fold_rel_context - (fun (na,c,t) (subst, n, avoid, inst, env) -> match na with + (fun (na,c,t) (subst, n, avoid, inst, env) -> +(* + match na with | Anonymous when not (Intset.mem n fv) -> (dummy_var::subst, n-1, avoid, inst, env) | _ -> +*) let id = next_name_away na avoid in ((mkVar id)::subst, n-1, id::avoid, mkRel n::inst, push_named (id,option_map (substl subst) c,substl subst t) env)) |