simplification de clenv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 3 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fa5eeaef3..79aa71c0f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -359,8 +359,8 @@ let general_elim_then_using
                    0 branchsigns.(i);
                branchnum = i+1;
                ity = ity;
-               largs = List.map (clenv_instance_term ce) largs;
-               pred = clenv_instance_term ce hd }
+               largs = List.map (clenv_nf_meta ce) largs;
+               pred = clenv_nf_meta ce hd }
     in 
     tac ba gl
   in
@@ -368,7 +368,8 @@ let general_elim_then_using
   let elimclause' =
     match predicate with
        | None   -> elimclause'
-       | Some p -> clenv_assign pmv p elimclause'
+       | Some p ->
+           clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause'
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl