From f393c2a0552d2c16715dbf163555662b7d20411d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Oct 2000 22:50:46 +0000
Subject: Bug ordre dans push_rels

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@677 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 8759158187..9fb5cc6c52 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -69,7 +69,7 @@ let push_rel_type sigma (na,t) env =
   push_rel_decl (na,make_typed t (get_sort_of env sigma t)) env
 
 let push_rels vars env =
-  List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars
+  List.fold_right (push_rel_type Evd.empty) vars env
 
 type inversion_status = Dep of constr option | NoDep
 
-- 
cgit v1.2.3