diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-13 16:21:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-13 16:21:53 +0000 |
| commit | afd11e5bfab001ed50381de5f15493fd76894f6b (patch) | |
| tree | da54db139bc59ae9f9addda8f45a65951e7dea4e /pretyping | |
| parent | 33d089aa4aaebd09e8f7facdabaa7b90a9369984 (diff) | |
Contournement du problème des evars de type, typées par défaut dans Type (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3239f0914..80a4a2ec0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -354,8 +354,8 @@ let rec pretype tycon env isevars lvar lmeta = function let pty = Retyping.get_type_of env (evars_of isevars) pred in let pj = { uj_val = pred; uj_type = pty } in - option_app (the_conv_x_leq env isevars pred) tycon; - pj + let _ = option_app (the_conv_x_leq env isevars pred) tycon + in pj with UserError _ -> findtype (i+1) in findtype 0 in let pj = j_nf_evar (evars_of isevars) pj in |