Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to coq/coq#17836 (sort poly) #28

Merged
merged 1 commit into from
Nov 7, 2023
Merged

Adapt to coq/coq#17836 (sort poly) #28

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/wp_rewrite.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ end = struct
let a = ca.(len - 1) in
let ca = Array.sub ca 0 (len - 1) in
Some (DApp, [mkApp (f, ca); a])
| Proj (p,c) -> pat_of_constr @@ mkApp (mkConst @@ Projection.constant p, [|c|])
| Proj (p,_,c) -> pat_of_constr @@ mkApp (mkConst @@ Projection.constant p, [|c|])
| Int i -> Some (DInt i, [])
| Float f -> Some (DFloat f, [])
| Array (_u,t,def,ty) -> Some (DArray, Array.to_list t @ [def ; ty])
Expand Down Expand Up @@ -281,6 +281,7 @@ let one_base (where: variable option) (tactic: trace tactic) (rewrite_database:
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let subst, ctx' = UnivGen.fresh_universe_context_set_instance rule.rew_ctx in
let subst = Sorts.QVar.Map.empty, subst in
let c' = Vars.subst_univs_level_constr subst rule.rew_lemma in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (rewrite rule.rew_l2r c' tac)
Expand Down Expand Up @@ -383,7 +384,7 @@ let to_raw_rew_rule (env: Environ.env) (sigma: Evd.evar_map) (hyp: Constrexpr.co
let econstr, context = Constrintern.interp_constr env sigma hyp in
let constr = EConstr.to_constr sigma econstr in
let univ_ctx = UState.context_set context in
let ctx = (DeclareUctx.declare_universe_context ~poly:false univ_ctx; Univ.ContextSet.empty) in
let ctx = (Global.push_context_set ~strict:true univ_ctx; Univ.ContextSet.empty) in
CAst.make ?loc:(Constrexpr_ops.constr_loc hyp) ((constr, ctx), true, Option.map (in_gen (rawwit wit_ltac)) None)

(**
Expand Down