aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-05-10Addedum to documentation of bullets: I now use the dedicated coq_exampleaspiwack
environment to display the example. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-10Documentation for Unfocused, braces and bullets.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15293 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Little bit of code refactoring in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15292 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Bug 2767pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Tactic unfold always asks for comma between names.pboutill
Else the parser takes "at" as a constant to unfold in "unfold plus at ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15290 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09End of Gtksourceview switch clean.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15289 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Removing dead code in CoqIDE made useless by the GtkSourceView switch.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15288 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Fixed access to environment variables in CoqIDE. Up to now, thoseppedrot
variables where set at compile time... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Rephrasing section on Sorts in CIC chapter, accordingly to discussionsherbelin
with Assia and Guillaume. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15284 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Ref. man., ch. CIC: clarifying the redundancy coming from having bothherbelin
Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15283 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Rewritten the autocompletion mechanism of CoqIDE, and stuffed itppedrot
into the ScriptView widget. The autocompletion algorithm may be a bit too greedy, so there are tests to do on huge buffers to check whether it is too slow and therefore we should fine-tune it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15282 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-06Cleanly rewritten the undo manager, which did not support redo and hadppedrot
a lot of deprecated code. Trying to be nicer with the built-in undo manager of GtkSourceView btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15281 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-05Renamed Undo to conform to CoqIDE widget naming convention. In addition,ppedrot
made various hack to handle GtkSourceView built-in undo/redo and made method types and names more compliant with the one of Gtk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15280 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-05Hack to handle trailing whitespace display in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15279 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-03Fixup r15251 second timepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15275 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added a bunch of new options relative to editor.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15274 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Better style handling in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15273 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Fixed previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15272 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Removed the useless use of a reference in preference handling.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Quick workaround to handle badly designed Sourceview package.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15270 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Coqide highligthing is back (done by gtksourceview).pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Coqide coq lexer put one tag at the end of a sentence.pboutill
And that's all ! It erase the possibility of code folding... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Source language and style are preferencespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15267 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02undoable_view is a source_viewpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15266 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Always add the Coq_config.dirs to xdg_dirspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Fixed #2769ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15264 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added an interface call to exit Coqtop nicely.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02A notion of permutation for lists modulo a setoid equalityletouzey
Contribution by Robbert Krebbers (Nijmegen University). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15261 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-01Cleaned the interface of analyzed_view in CoqIDE. A lot of methodsppedrot
have been made private, for the sake of readability and conciseness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15260 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30This is a tentative bugfix for the numerous GText.iter erros occuring in CoqIDE.ppedrot
Because of the previous highlighting process, whenever this process would fail on an unterminated phrase, a thread would wait 1.5s and retry once. This thread conflicted in particular with any subsequent non-atomic use of iters. Actually, this seems pretty useless, so until using SourceView, this sould do the work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15259 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30Fixed an accelerator parsing error in CoqIDE introduced in r15254ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15258 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-28Fix make install after emacs mode troll (r15251)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15256 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Configure asks for lablgtk >= 2.12 with gtksourceview2pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Coqide MacOS integration refreshpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Partial revert of r15148 in order to compile with Camlp4pboutill
+ comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
There is a warning if the term is more precise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Removed the quasi-useless gtk2rc file and the documentation that went with ↵ppedrot
it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-26migration of g_obligations.ml4, ocamlbuild sideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15249 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-26migrate g_obligations.ml4 in parsingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-26Program: avoid staying in program mode after a failed Program commandletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15247 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-25Avoid unneeded head-normalizations in coercion code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15246 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-25Do not delta-head-normalize the proposition argument of sigma types during ↵msozeau
coercion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15245 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-24Removed a unused and troublesome feature in CoqIDE that handled shortcuts ↵ppedrot
the old way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15244 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Fix ocamlbuild compilation: remove subtac from *.itargetletouzey
With this subtac forgotten target, the coqdepdeps rule was unsatisfiable, blocking the ocamlbuild compilation on a nasty circular dependency error on initial.coq (sic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15240 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23correct abort in Function when a proof of inversion failsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15239 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Fixed bad gravity of mark that would make CoqIDE loop whenever Replace All ↵ppedrot
was used with a self-contained replacement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15237 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Cleaning a bit previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15235 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead ↵ppedrot
code that used to serve as such a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15234 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-20Cleaning up widget code and using a naming convention for such files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15232 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-15 04:06:17 +0000