diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-20 17:40:50 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-20 17:40:50 +0000 |
| commit | 300bf8df2e36b2a25617e49bb80e330491bb0b8c (patch) | |
| tree | d5e5d312028bc9de50b80d29370da00dfa714de7 /contrib/subtac | |
| parent | 9c93d269e5d963f262383451ccdf8e98af2237d3 (diff) | |
Fix minor bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8069 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/interp.ml | 2 | ||||
| -rw-r--r-- | 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 1be49ef27..83f26ced1 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 c1996953b..fa5dc5bec 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) -> |