From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 09:04:17 +0200 Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5. - Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test. --- tactics/eqschemes.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'tactics/eqschemes.ml') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4..e39159fb8 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -89,6 +89,11 @@ let get_coq_eq ctx = with Not_found -> error "eq not found." +let univ_of_eq env eq = + match kind_of_term (Retyping.get_type_of env Evd.empty eq) with + | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + | _ -> assert false + (**********************************************************************) (* Check if an inductive type [ind] has the form *) (* *) @@ -744,7 +749,7 @@ let build_congr env (eq,refl,ctx) ind = let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -752,6 +757,7 @@ let build_congr env (eq,refl,ctx) ind = let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda varB (mkSort (Type uni)) -- cgit v1.2.3