diff options
| author | Pierre-Marie Pédrot | 2020-12-11 21:09:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-14 09:54:46 +0100 |
| commit | 161b7b47f7f87c33f1fa6269248d5f8b6b4926d9 (patch) | |
| tree | 0aae961fb08b8c59ace1cd906dea0b930a297b85 /proofs | |
| parent | 981146bbc716494ba9ced0d6b403923b293cdec1 (diff) | |
Make the clenv type private and provide a creation function.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/clenv.mli | 4 |
2 files changed, 10 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f47ed0fc4b..23ae9d04c4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -39,6 +39,13 @@ type clausenv = { templval : constr freelisted; templtyp : constr freelisted } +let mk_clausenv env evd templval templtyp = { + env; evd; templval; templtyp; +} + +let update_clenv_evd clenv evd = + mk_clausenv clenv.env evd clenv.templval clenv.templtyp + let cl_env ce = ce.env let cl_sigma ce = ce.evd diff --git a/proofs/clenv.mli b/proofs/clenv.mli index a72c8c5e1f..bfdc5cdd8c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -22,7 +22,7 @@ open Tactypes (** {6 The Type of Constructions clausale environments.} *) -type clausenv = { +type clausenv = private { env : env; (** the typing context *) evd : evar_map; (** the mapping from metavar and evar numbers to their types and values *) @@ -30,6 +30,8 @@ type clausenv = { out *) templtyp : constr freelisted (** its type *)} +val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv +val update_clenv_evd : clausenv -> evar_map -> clausenv (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr |