diff options
| author | barras | 2005-06-07 21:38:40 +0000 |
|---|---|---|
| committer | barras | 2005-06-07 21:38:40 +0000 |
| commit | 9061ea66e66a7fe7ebd299d606d73514abc66d0e (patch) | |
| tree | b5c06a3762b8912f056fc28f144494cd2329ff2e /pretyping/pretyping.ml | |
| parent | 84d8767bbe195c664e0237f9eaedfaf7a977efa4 (diff) | |
reparations de quelques petits bugs d\'unification + introduction de la notion de variable de sortes (mais pas encore utilise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6101396a40..d7a5da4cc3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -532,10 +532,10 @@ let rec pretype tycon env isevars lvar = function Cases.pred_case_ml env (evars_of !isevars) false indt (0,fj.uj_type) in - if has_undefined_evars !isevars pred then - use_constraint () - else + if is_ground_term !isevars pred then true, pred + else + use_constraint () with Cases.NotInferable _ -> use_constraint () in @@ -754,7 +754,7 @@ let rec pretype tycon env isevars lvar = function let pred = Cases.pred_case_ml (* eta-expanse *) env (evars_of !isevars) isrec indt (i,fj.uj_type) in - if has_undefined_evars !isevars pred then findtype (i+1) + if not (is_ground_term !isevars pred) then findtype (i+1) else let pty = Retyping.get_type_of env (evars_of !isevars) pred in |