From a62942ebef6f02e0a9f9783f4a8cb0ff80eb077d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 25 May 2023 16:14:03 +0200 Subject: [PATCH] Fix datatype comparisons for theory replays We do not need to check the inductive schemas: - if the constructors are compatible, so are the schemas, - anyway, they are going to be checked right after, and - at that point, they are not convertible because they come from incomaptible enclosing theories. Fix #381 --- src/ecTheoryReplay.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 488fae7c6f..99111f8fb2 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -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); @@ -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