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.mli | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index acc1bfee8a..7e53964642 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *) -val add_typedef : Constant.t -> constant_body -> ml_type -> unit -val lookup_typedef : Constant.t -> constant_body -> ml_type option +val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit +val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option -val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit -val lookup_cst_type : Constant.t -> constant_body -> ml_schema option +val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit +val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option |