From 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 02:27:54 -0400
Subject: [ComDefinition] Split program from regular declarations

Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.

Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.

This PR is in preparation for that.
---
 plugins/funind/gen_principle.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 28cf5c7d98..4242da2802 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -375,7 +375,6 @@ let register_struct is_rec fixpoint_exprl =
       | None ->
         CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
     ComDefinition.do_definition
-      ~program_mode:false
       ~name:fname.CAst.v
       ~poly:false
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-- 
cgit v1.2.3