From aab16ea645fefd71b6bd0fdb155a076640ab0d4e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 2 Aug 2010 21:14:19 +0000
Subject: Fix [clenv_missing] to compute a better approximation of missing
 dependent arguments. It breaks compatibility as some [apply with] clauses are
 not necessary anymore. Typically when applying [f_equal], the domain type of
 the function can be infered even if it does not appear directly in the
 conclusion of the goal. Fixes bug #2154.

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dfd92f0c17..8898e5989a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -717,6 +717,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let understand_judgment_tcc evdref env c =
     let j = pretype empty_tycon env evdref ([],[]) c in
+    evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env !evdref;
     j_nf_evar !evdref j
 
   (* Raw calls to the unsafe inference machine: boolean says if we must
-- 
cgit v1.2.3