diff options
| -rw-r--r-- | CREDITS | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 13 | ||||
| -rw-r--r-- | test-suite/ssr/case_polyuniv.v | 12 |
3 files changed, 23 insertions, 3 deletions
@@ -155,6 +155,7 @@ of the Coq Proof assistant during the indicated time: Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now) Clément Renard (INRIA, 2001-2004) Talia Ringer (University of Washington, 2019) + Andreas Lynge (Aarhus University, 2019) Claudio Sacerdoti Coen (INRIA, 2004-2005) Amokrane Saïbi (INRIA, 1993-1998) Vincent Semeria (2018) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index dbc9bb24c5..3a0868b7e4 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -383,15 +383,22 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in let gl, eq = get_eq_type gl in - let gen_eq_tac, gl = + let gen_eq_tac, eq_ty, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in - apply_type new_concl [erefl], gl in + let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in + let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in + let gen_eq_tac s = + let open Evd in + let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in + apply_type new_concl [erefl] { s with sigma } + in + gen_eq_tac, eq_ty, gl in let rel = k + if c_is_head_p then 1 else 0 in - let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in + let src, gl = mkProt eq_ty EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl diff --git a/test-suite/ssr/case_polyuniv.v b/test-suite/ssr/case_polyuniv.v new file mode 100644 index 0000000000..8774e191c1 --- /dev/null +++ b/test-suite/ssr/case_polyuniv.v @@ -0,0 +1,12 @@ +Require Import ssreflect. + +Set Universe Polymorphism. + +Cumulative Variant paths {A} (x:A) : A -> Type + := idpath : paths x x. + +Register paths as core.eq.type. +Register idpath as core.eq.refl. + +Lemma case_test (b:bool) : paths b b. +Proof. case B:b; reflexivity. Qed. |