From a6b6bf31121d975c915c01f501618d97df7879fb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 9 May 2015 09:00:51 +0200 Subject: Extended inline asm: revised treatment of clobbered registers. - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting --- extraction/extraction.v | 3 --- 1 file changed, 3 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 4c400036..f7e99545 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -77,9 +77,6 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". -(* Bounds *) -Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber". - (* SimplExpr *) Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. -- cgit