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
---
 plugins/subtac/subtac_pretyping_F.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 47882e771a..b49190d446 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -575,15 +575,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    evdref := consider_remaining_unif_problems env !evdref;
-    if resolve_classes then
-      (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+    in
+      if resolve_classes then
+	evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
-       evdref := consider_remaining_unif_problems env !evdref);
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-    if fail_evar then check_evars env Evd.empty !evdref c;
-    c
+      evdref := consider_remaining_unif_problems env !evdref;
+      let c = if expand_evar then nf_evar !evdref c' else c' in
+      if fail_evar then check_evars env Evd.empty !evdref c;
+      c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
-- 
cgit v1.2.3