search

jscert / jsexplain

Apache License 2.0
26 stars 4 forks source link

Remove coq prefix #32

Closed barockobamo closed 5 years ago

barockobamo commented 5 years ago

Grep and Replace 'Coq_' prefix in source folder. make test command behave fine. Readme section has been removed as requested. If you want to check it.

IgnoredAmbience commented 5 years ago

Yes, by block I meant the begin...end block. GitHub doesn't allow review comments on lines of code that weren't present in the patch, so I was unable to comment at the function definition location.

On 19 September 2018 13:10:06 BST, barockobamo notifications@github.com wrote:

barockobamo commented on this pull request.

@@ -1139,7 +1139,7 @@ and js_of_expression (sm : shadow_map) ctx dest e = let cstr_fullname = if cstr_fullname = "[]" then "mk_nil" else if cstr_fullname = "::" then "mk_cons"

  • else begin ( rename the constructor to remove "Coq_" prefix )
  • else begin ( rename the constructor to remove "" prefix )

Isn't the end of the code missing ? Is this code : What you mean ? let rename_constructor s = s

-- You are receiving this because your review was requested. Reply to this email directly or view it on GitHub: https://github.com/jscert/jsexplain/pull/32#discussion_r218777365

-- Sent from my Android device with K-9 Mail. Please excuse my brevity.

barockobamo commented 5 years ago

Maybe we can just remove the function, there are only 3 calls in the module. Is it usefull outside of it ?

IgnoredAmbience commented 5 years ago

Yes, removing that function should be good.