diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 02:27:54 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 (patch) | |
| tree | 020c8aded6b220f4bc022555673e0737445e9107 /plugins | |
| parent | 76115e703751cfde99d7e86be9eea8fb32398e8a (diff) | |
[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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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) |