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#18938 (EConstr.ERelevance) #43

Merged
merged 1 commit into from
Apr 23, 2024
Merged

Adapt to coq/coq#18938 (EConstr.ERelevance) #43

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
14 changes: 7 additions & 7 deletions src/reify.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ open Constr
open EConstr
open Names

let mkArrow x y = mkArrow x Sorts.Relevant y
let mkArrow x y = mkArrow x ERelevance.relevant y

(* pick an element in an hashtbl *)
let hashtbl_pick t = Hashtbl.fold (fun i x -> function None -> Some (i,x) | acc -> acc) t None
Expand Down Expand Up @@ -215,8 +215,8 @@ end = struct
t := ((x,j,Lazy.force y)::l,i+1); j

let to_env t typ def = match fst !t with
| [] -> mkLambda (Context.make_annot Anonymous Sorts.Relevant,Lazy.force Coq.positive,def)
| [_,_,x] -> mkLambda (Context.make_annot Anonymous Sorts.Relevant,Lazy.force Coq.positive,x)
| [] -> mkLambda (Context.make_annot Anonymous ERelevance.relevant,Lazy.force Coq.positive,def)
| [_,_,x] -> mkLambda (Context.make_annot Anonymous ERelevance.relevant,Lazy.force Coq.positive,x)
| (_,_,x)::q ->
Reification.sigma_get typ x
(List.fold_left
Expand Down Expand Up @@ -335,10 +335,10 @@ let reify_goal ops =

(* reified goal conclusion: add the relation over the two evaluated members *)
let reified =
mkNamedLetIn sigma (Context.make_annot tenv_name Sorts.Relevant) tenv (mkArrow (Lazy.force Coq.positive) typ) (
mkNamedLetIn sigma (Context.make_annot env_name Sorts.Relevant) tenv' (Reification.env_type gph) (
mkNamedLetIn sigma (Context.make_annot ln Sorts.Relevant) lv x (
mkNamedLetIn sigma (Context.make_annot rn Sorts.Relevant) rv x (
mkNamedLetIn sigma (Context.make_annot tenv_name ERelevance.relevant) tenv (mkArrow (Lazy.force Coq.positive) typ) (
mkNamedLetIn sigma (Context.make_annot env_name ERelevance.relevant) tenv' (Reification.env_type gph) (
mkNamedLetIn sigma (Context.make_annot ln ERelevance.relevant) lv x (
mkNamedLetIn sigma (Context.make_annot rn ERelevance.relevant) rv x (
(mkApp (rel, [|Reification.typ gph env_ref src; Reification.typ gph env_ref tgt;l;r|]))))))
in
(try
Expand Down
Loading