From 75cad06804697eab5456166185a3413fb48eb21a Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 10 Oct 2001 18:39:01 +0000 Subject: Incompatibilité entre la prise en compte des univers au niveau des tactiques et le test de conversion qui oublie la cumulativité MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 4 +++- tactics/wcclausenv.ml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'tactics') 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 -- cgit v1.2.3