diff options
| author | Hugo Herbelin | 2020-04-08 09:57:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-15 19:43:28 +0200 |
| commit | 79ccbe6b2b73409d7ce5e0e5797320b6e2fd0dd2 (patch) | |
| tree | 64e2fa14f8343ec355284888ea4ddeb2f3e0fd45 /interp/constrintern.ml | |
| parent | c7ed001b310583b8087574cd64ab6bed9b321f86 (diff) | |
Making type interning_data abstract in constrintern.ml.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 75fda5d239..7431058849 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -186,6 +186,9 @@ let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map) impls +let extend_internalization_data (r, impls, scopes) impl scope = + (r, impls@[impl], scopes@[scope]) + (**********************************************************************) (* Contracting "{ _ }" in notations *) |