diff options
| author | Pierre-Marie Pédrot | 2019-05-15 23:50:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:14:19 +0200 |
| commit | 801aed67a90ec49c15a4469e1905aa2835fabe19 (patch) | |
| tree | 9da139e5e0e5ecd8ba74806d2baa1225cee2e720 /plugins/extraction/table.ml | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 399a77c596..4e229a94b6 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -109,7 +109,7 @@ let labels_of_ref r = (*s Constants tables. *) -let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t) let init_typedefs () = typedefs := Cmap_env.empty let add_typedef kn cb t = typedefs := Cmap_env.add kn (cb,t) !typedefs @@ -120,7 +120,7 @@ let lookup_typedef kn cb = with Not_found -> None let cst_types = - ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) + ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t) let init_cst_types () = cst_types := Cmap_env.empty let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types let lookup_cst_type kn cb = |