From 1a7466be726edfc883412ba511e2c84f0e0071fc Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 15 Mar 2010 19:35:45 +0000
Subject: Fix splitting evars tactics and stop dropping evar constraints when
 building a new goal evar defs. Allow customization of the reduction function
 applied to subtac obligations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 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 013270a6a7..8654ca9479 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -677,9 +677,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (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 := 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;
-- 
cgit v1.2.3