diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index bfdc5cdd8c..6e472da452 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -28,7 +28,9 @@ type clausenv = private { types and values *) templval : constr freelisted; (** the template which we are trying to fill out *) - templtyp : constr freelisted (** its type *)} + templtyp : constr freelisted; (** its type *) + cache : Reductionops.meta_instance_subst; (* Reductionops.create_meta_instance_subst evd) *) +} val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv val update_clenv_evd : clausenv -> evar_map -> clausenv |