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 | |
| 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')
| -rw-r--r-- | plugins/extraction/extraction.mli | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 8 |
3 files changed, 8 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index d27c79cb62..bf98f8cd70 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -16,9 +16,9 @@ open Environ open Evd open Miniml -val extract_constant : env -> Constant.t -> constant_body -> ml_decl +val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl -val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec +val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) 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 = 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 |