diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 399a77c596..c2c48f9565 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -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 = @@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) |