diff options
| author | barras | 2004-03-08 17:53:03 +0000 |
|---|---|---|
| committer | barras | 2004-03-08 17:53:03 +0000 |
| commit | 4204aa78b9ae084d98bc7a585ec199f94bb7ece5 (patch) | |
| tree | 96314cf740895fb11efe25bf85c001b051583d9d /pretyping | |
| parent | dbcb155c3b52265b88929a8a5f05b354e36c69db (diff) | |
correction de bugs des points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e1f0da13b5..8bd6a1a018 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -387,7 +387,7 @@ and share_names tenv n l avoid env c t = if !Options.v7 && n=0 then let c = detype tenv avoid env c in let t = detype tenv avoid env t in - (l,c,t) + (List.rev l,c,t) else match kind_of_term c, kind_of_term t with | Lambda (na,t,c), Prod (na',t',c') -> @@ -420,7 +420,7 @@ and share_names tenv n l avoid env c t = if n>0 then warning "Detyping.detype: cannot factorize fix enough"; let c = detype tenv avoid env c in let t = detype tenv avoid env t in - (l,c,t) + (List.rev l,c,t) and detype_eqn tenv avoid env constr construct_nargs branch = let make_pat x avoid env b ids = |