diff options
| author | Gaëtan Gilbert | 2019-05-21 12:41:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-21 12:41:57 +0200 |
| commit | afb1a427debbc32aef1b2df0b31aa9cf8938b687 (patch) | |
| tree | acaa552dfc9a6f72bf90303f1d437b8856a9112a /plugins/extraction/table.mli | |
| parent | 897088fb8f4769bacca9fc289387096283835cd6 (diff) | |
| parent | e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c (diff) | |
Merge PR #10174: Further cleanup of the side-effect machinery
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
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 |