diff options
| -rw-r--r-- | tactics/eqschemes.ml | 8 | ||||
| -rw-r--r-- | test-suite/success/Scheme.v | 23 |
2 files changed, 30 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4a..e39159fb82 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)) diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index dd5aa81d1d..855f26698c 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -2,3 +2,26 @@ Scheme Induction for eq Sort Prop. Check eq_ind_dep. + +(* This was broken in v8.5 *) + +Set Rewriting Schemes. +Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a. +Unset Rewriting Schemes. + +Check myeq_rect. +Check myeq_ind. +Check myeq_rec. +Check myeq_congr. +Check myeq_sym_internal. +Check myeq_rew. +Check myeq_rew_dep. +Check myeq_rew_fwd_dep. +Check myeq_rew_r. +Check internal_myeq_sym_involutive. +Check myeq_rew_r_dep. +Check myeq_rew_fwd_r_dep. + +Set Rewriting Schemes. +Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. +Unset Rewriting Schemes. |