From 300bf8df2e36b2a25617e49bb80e330491bb0b8c Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 20 Feb 2006 17:40:50 +0000
Subject: Fix minor bug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8069 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/interp.ml          | 2 +-
 contrib/subtac/subtac_coercion.ml | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
index 1be49ef275..83f26ced1e 100644
--- a/contrib/subtac/interp.ml
+++ b/contrib/subtac/interp.ml
@@ -268,7 +268,7 @@ let rec pretype tycon env isevars lvar = function
 	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
             let resty =
               whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
-	    let coercef, resty = Subtac_coercion.mu env isevars resj in
+	    let coercef, resty = Subtac_coercion.mu env isevars resty in
 	      match kind_of_term resty with
 	      | Prod (na,c1,c2) ->
 		  let hj = pretype (mk_tycon c1) env isevars lvar c in
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index c1996953bb..fa5dc5bec7 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -84,8 +84,7 @@ let sort_rel s1 s2 =
     | Type _, Prop Null -> Prop Null
     | _, Type _ -> s2
 
-let rec mu env isevars j = 
-  let {uj_val = v; uj_type = t} = j in
+let rec mu env isevars t =   
   let rec aux v = 
     match disc_subset v with
       Some (u, p) -> 
-- 
cgit v1.2.3