Julien Narboux
Julien Narboux
I have seen some people disturbed by the fact that "assumption" is colored in red, whereas other tactics are not. I don't get why some tactics appear in red (tauto,...
Clicking on the Js+Coq (or Wa+Coq) button opens Jscoq in the current window. I have seen some people clicking on it by mistake and loosing what they typed in the...
Hi, Jscoq can be used by beginners in a tutorial, the teacher showing examples on the beamer. In this setting, having nice \forall and \P etc, is not helping because...
I think the button to show/hide the right hand side pane is not very intuitive. I think arrows pointing left/or right like in the following screenshot is more standard. 
When I try to get the type of an element in the goal view, jscoq provides the result of a Check, not the type in the real context. Here I...
For beginner, it would nice to have tooltips for the navigation menus, so they get quickly what the button is supposed to do.
Hi, I think it should be trivial to add some buttons for the standard function of loading/saving/saving as. When trying to use the shortcuts on chrome on mac, I get...
Sometimes On conclut par .... displays linarith failed to find a contradiction, where as the goal as nothing to do with linear arithmetic,I understand that the tactic tries different things,...
In this context: x_mem: f x ∈ B ∪ B' ⊢ x ∈ f ⁻¹' B ∪ f ⁻¹' B' Help suggest to use We conclude with x_mem. We conclude...