From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 3 Mar 2019 21:03:37 +0100 Subject: Change the representation of kernel case. We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval. --- engine/evd.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index a6d55c2615..ec9ae6fca9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -772,8 +772,8 @@ module MiniEConstr : sig (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt - val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert - val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert + val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert + val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> -- cgit v1.2.3 From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 11 Dec 2020 13:20:54 +0100 Subject: Remove redundant univ and parameter info from CaseInvert --- engine/evd.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index ec9ae6fca9..58f635b7bd 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -772,8 +772,8 @@ module MiniEConstr : sig (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt - val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert - val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert + val of_case_invert : constr pcase_invert -> econstr pcase_invert + val unsafe_to_case_invert : econstr pcase_invert -> constr pcase_invert val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> -- cgit v1.2.3