diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /engine/evd.mli | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
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.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 -> |