diff options
| author | herbelin | 2001-03-14 21:21:12 +0000 |
|---|---|---|
| committer | herbelin | 2001-03-14 21:21:12 +0000 |
| commit | af22eb086aaec3551ccc9dd6bcf754c38f933eb6 (patch) | |
| tree | cec742d4996063007a23857d129692218050bc37 /pretyping | |
| parent | a9868b434b8fea32bea4471e3cb8c5334cbc0fac (diff) | |
Prise en compte des Let dans l'instance des evars
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1465 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c155c45554..d7df2507cd 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -61,7 +61,7 @@ let dummy_sort = mkType dummy_univ let make_evar_instance env = fold_named_context - (fun env (id, b, _) l -> if b=None then mkVar id :: l else l) + (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*)) env [] (* Declaring any type to be in the sort Type shouldn't be harmful since @@ -189,6 +189,7 @@ let real_clean isevars sp args rhs = else begin let (sigma,rc) = do_restrict_hyps !isevars ev args' in isevars := sigma; + rc end else @@ -204,18 +205,18 @@ let make_evar_instance_with_rel env = let n = rel_context_length (rel_context env) in let vars = fold_named_context - (fun env (id,b,_) l -> if b=None then mkVar id :: l else l) + (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*)) env [] in snd (fold_rel_context - (fun env (_,b,_) (i,l) -> (i-1, if b=None then mkRel i :: l else l)) + (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*))) env (n,vars)) let make_subst env args = snd (fold_named_context (fun env (id,b,c) (args,l as g) -> match b, args with - | None, a::rest -> (rest, (id,a)::l) - | Some _, _ -> g + | (* None *) _ , a::rest -> (rest, (id,a)::l) +(* | Some _, _ -> g*) | _ -> anomaly "Instance does not match its signature") env (List.rev args,[])) |