diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 8 |
3 files changed, 23 insertions, 9 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 56f17703ff..6c7b4702b6 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -194,8 +194,8 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRVar id = DAst.make @@ GRef (VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) -let mkRType = DAst.make @@ GSort (GType []) -let mkRProp = DAst.make @@ GSort (GProp) +let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) +let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) @@ -871,8 +871,8 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort GProp -let mkCType loc = CAst.make ?loc @@ CSort (GType []) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) @@ -1119,6 +1119,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let pat = interp_cpattern gl t None in (* UGLY API *) + let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 @@ -1253,6 +1254,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in @@ -1265,6 +1267,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in 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/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 538d0c4e9a..91905d277c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -336,14 +336,14 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = + let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in @@ -619,7 +619,11 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in let rwtac gl = let rx = Option.map (interp_rpattern gl) grx in + let gl = match rx with + | None -> gl + | Some (s,_) -> pf_merge_uc_of s gl in let t = interp gt gl in + let gl = pf_merge_uc_of (fst t) gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt |