Skip to content

Fix datatype comparisons for theory replays #385

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

Merged
strub merged 1 commit into from
May 25, 2023
Merged

Fix datatype comparisons for theory replays #385

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: 1 addition & 4 deletions src/ecTheoryReplay.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,7 @@ let constr_compatible exn env cs1 cs2 =

let datatype_compatible exn hyps ty1 ty2 =
let env = EcEnv.LDecl.toenv hyps in
constr_compatible exn env ty1.tydt_ctors ty2.tydt_ctors;
error_body exn (EcReduction.is_conv hyps ty1.tydt_schcase ty2.tydt_schcase);
error_body exn (EcReduction.is_conv hyps ty1.tydt_schelim ty2.tydt_schelim)
constr_compatible exn env ty1.tydt_ctors ty2.tydt_ctors

let record_compatible exn hyps f1 pr1 f2 pr2 =
error_body exn (EcReduction.is_conv hyps f1 f2);
Expand Down Expand Up @@ -118,7 +116,6 @@ let tydecl_compatible env tyd1 tyd2 =
| `Abstract _, _ -> () (* FIXME Sp.t *)
| _, _ -> tybody_compatible exn hyps ty_body1 ty_body2


(* -------------------------------------------------------------------- *)
let expr_compatible exn env s e1 e2 =
let f1 = EcFol.form_of_expr EcFol.mhr e1 in
Expand Down