diff options
| author | Maxime Dénès | 2019-01-25 17:47:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-05 09:36:51 +0100 |
| commit | 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 (patch) | |
| tree | e6697a39eb0cfb7b45a08e88dd08ad2fe7eedadb /engine | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
Make Program a regular attribute
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 6 | ||||
| -rw-r--r-- | engine/evarutil.mli | 1 |
2 files changed, 5 insertions, 2 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index db56d0628f..d70c009c6d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -337,6 +337,7 @@ type naming_mode = | KeepUserNameAndRenameExistingEvenSectionNames | KeepExistingNames | FailIfConflict + | ProgramNaming let push_rel_decl_to_named_context ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) @@ -364,7 +365,7 @@ let push_rel_decl_to_named_context using this function. For now, we only attempt to preserve the old behaviour of Program, but ultimately, one should do something about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid + if hypnaming = ProgramNaming then next_name_away na avoid else (* id_of_name_using_hdchar only depends on the rel context which is empty here *) @@ -372,7 +373,8 @@ let push_rel_decl_to_named_context in match extract_if_neq id na with | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || - hypnaming = KeepUserNameAndRenameExistingButSectionNames && + (hypnaming = KeepUserNameAndRenameExistingButSectionNames || + hypnaming = ProgramNaming) && not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 0e67475778..23b240f1a0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -38,6 +38,7 @@ type naming_mode = | KeepUserNameAndRenameExistingEvenSectionNames | KeepExistingNames | FailIfConflict + | ProgramNaming val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> |