Conversation
|
Thank you Antoine for your PR but there seems to be unjustified changes. Please minimize the diff (be careful with changes in the indentation). |
Could you be clearer on what you call unjustified ? Is there something apart from the two lines where I changed the indentation to match the rest of the file ? |
|
When I look at https://github.com/Deducteam/lambdapi/pull/1346/files, I see many "changes" from line 311 that do not seem necessary. Perhaps there is actually no changes except in the indentation. But this is the kind of changes that should be avoided in order to more easily track changes back in time when something gets broken. See for instance the "blame" function of Github on https://github.com/Deducteam/lambdapi/blame/master/src/export/coq.ml. |
I never thought about it that way ! Indeed important then. |
| | P_symbol | ||
| { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; | ||
| p_sym_trm; p_sym_prf=_; p_sym_def } -> | ||
| if not (StrSet.mem p_sym_nam.elt !erase) then |
There was a problem hiding this comment.
There is no need to change the command function here and above.
src/export/coq.ml
Outdated
| Stream.iter consume (Parser.parse_file f) | ||
|
|
||
| (** true if id is in the image of !rmap *) | ||
| let is_existing_rocq_id id = StrMap.exists (fun _ id' -> id == id') !rmap |
There was a problem hiding this comment.
Can be unfolded because it is short and used only once.
agontard
force-pushed
the
name_collisions
branch
from
7629b94 to
dd77334
Compare
|
@fblanqui In the end just one line to change. I tested that it works, through checking Real_def/Real_with_N without mapping for "+", which normally creates a name collision because of the renaming to "add" in renaming.lp in hol2dk, which is also the name of a variable in a proof which uses "+". |
2 participants
Uh oh!
There was an error while loading. Please reload this page.