diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:17:58 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:17:58 +0000 |
commit | c1234a327b8ef2b52af1410dace719000c360f53 (patch) | |
tree | 34bcfe5d05b3ff2c1d4ad41fa6e29ff44a5fb908 /pretyping | |
parent | e79b800bec660dc2724fa70c33f4e435ddbf885c (diff) |
More on r14536 (an unused pattern-matching remained in the commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/evd.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index cb44c926f..c73ff91a1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -168,12 +168,9 @@ module EvarInfoMap = struct (* Note: let-in contributes to the instance *) let make_evar_instance sign args = let rec instrec = function - | (id,_,_) :: sign, c::args -> - (match kind_of_term c with - | Var id' when id = id' -> instrec (sign,args) - | _ -> (id,c) :: instrec (sign,args)) + | (id,_,_) :: sign, c::args when isVarId id c -> instrec (sign,args) | (id,_,_) :: sign, c::args -> (id,c) :: instrec (sign,args) - | [],[] -> [] + | [],[] -> [] | [],_ | _,[] -> anomaly "Signature and its instance do not match" in instrec (sign,args) |