diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-10 18:39:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-10 18:39:01 +0000 |
| commit | 75cad06804697eab5456166185a3413fb48eb21a (patch) | |
| tree | daa86c2d63abcce49b7d607ee43fcebd82bc11a7 /tactics | |
| parent | f1778f0e830c50aaec250916f14e202d95960414 (diff) | |
Incompatibilité entre la prise en compte des univers au niveau des tactiques et le test de conversion qui oublie la cumulativité
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/wcclausenv.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e7673944e..8a8025f12 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1597,7 +1597,9 @@ let elim_scheme_type elim t gl = let clause = mk_clenv_type_of wc elim in match kind_of_term (last_arg (clenv_template clause).rebus) with | IsMeta mv -> - let clause' = clenv_unify (clenv_instance_type clause mv) t clause in + let clause' = + (* t is inductive, then CUMUL or CONV is irrelevant *) + clenv_unify CUMUL t (clenv_instance_type clause mv) clause in elim_res_pf kONT clause' gl | _ -> anomaly "elim_scheme_type" diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 63504956c..2c791f3bb 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -93,7 +93,7 @@ let clenv_constrain_with_bindings bl clause = let sigma = Evd.empty in let k_typ = nf_betaiota (clenv_instance_type clause k) in let c_typ = nf_betaiota (w_type_of clause.hook c) in - matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t + matchrec (clenv_assign k c (clenv_unify CUMUL c_typ k_typ clause)) t in matchrec clause bl |