diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/table.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index f95f81ee9..ce2a99c6d 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -337,14 +337,22 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let (inline_extraction,_) = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); classify_function = (fun (_,o) -> Substitute o); - subst_function = (fun (_,s,(b,l)) -> (b,(List.map (subst_global s) l))) } + (*CSC: The following substitution may istantiate a realized parameter. + The right solution would be to make the substitution erase the + realizer from the table. However, this is not allowed by Coq. + In this particular case, though, keeping the realizer is place seems + to be harmless since the current code looks for a realizer only + when the constant is a parameter. However, if this behaviour changes + subtle bugs can happear in the future. *) + subst_function = + (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))} let _ = declare_summary "Extraction Inline" { freeze_function = (fun () -> !inline_table); |