From 042a9e9156c183e705a5d5dddd4f2842fa57b943 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 7 Mar 2010 22:51:23 +0000
Subject: Reorder resolution of type class and unification constraints. Fix a
 bug in dependent elimination when treating defined variables in the context.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bed4d834d2..013270a6a7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -677,7 +677,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env evdref lvar c).utj_val 
     in
     if resolve_classes then (
-      evdref := consider_remaining_unif_problems env !evdref;
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref);
@@ -694,10 +693,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let evdref = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let evd = consider_remaining_unif_problems env !evdref in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
-      ~fail:true env evd
+      ~fail:true env !evdref
     in
+    let evd = consider_remaining_unif_problems env evd in
     let j = j_nf_evar evd j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
-- 
cgit v1.2.3