From 700bbf17a9fb585f6890cd1fd71a8ced8551cd16 Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 5 Oct 2010 08:32:43 +0000
Subject: Auto-inlining of f_terminate in Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/recdef.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c42ecac421..057ffb9b32 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1425,6 +1425,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+    let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in 
 (*     message "start second proof"; *)
     let stop = ref false in
     begin
-- 
cgit v1.2.3