From 8ff2de8c01b3ba3563517627b1f5c9eb2c4bcb77 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 14 Mar 2012 09:53:06 +0000
Subject: Final part of moving Program code inside the main code. Adapted
 add_definition/fixpoint and parsing of the "Program" prefix.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun.ml         | 8 ++------
 plugins/funind/indfun_common.mli | 4 ++--
 2 files changed, 4 insertions(+), 8 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 449dcd20eb..31814b141e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -361,12 +361,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
-	let ce,imps =
-	  Command.interp_definition bl None body (Some ret_type)
-	in
-	Command.declare_definition
-	  fname (Decl_kinds.Global,Decl_kinds.Definition)
-	  ce imps (fun _ _ -> ())
+	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
+	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
 	Command.do_fixpoint fixpoint_exprl
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index f6500f74de..bb59a5c9cc 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -55,7 +55,7 @@ val jmeq_refl : unit -> Term.constr
 val new_save_named : bool -> unit
 
 val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  Tacexpr.declaration_hook -> unit
+  unit Tacexpr.declaration_hook -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
@@ -63,7 +63,7 @@ val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_k
 val get_proof_clean : bool ->
   Names.identifier *
     (Entries.definition_entry * Decl_kinds.goal_kind *
-       Tacexpr.declaration_hook)
+      unit Tacexpr.declaration_hook)
 
 
 
-- 
cgit v1.2.3