diff options
| author | herbelin | 2003-01-31 16:47:23 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-31 16:47:23 +0000 |
| commit | 253e5c3e2fe8815a15b55728039d789298166137 (patch) | |
| tree | 1c141041690e35529156c01616386d5c4f11ce72 | |
| parent | f358f9ac760e24a9e82d44e0c5da8c49e145913c (diff) | |
Unification plus efficace vis à vis du LetIn
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3638 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 623d0e99d5..42af2bfe62 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -32,6 +32,7 @@ let flex_kind_of_term c l = | Rel n -> MaybeFlexible c | Var id -> MaybeFlexible c | Lambda _ when l<>[] -> MaybeFlexible c + | LetIn _ -> MaybeFlexible c | Evar ev -> Flexible ev | _ -> Rigid c @@ -40,6 +41,7 @@ let eval_flexible_term env c = | Const c -> constant_opt_value env c | Rel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v | Var id -> let (_,v,_) = lookup_named id env in v + | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | _ -> assert false (* |