aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-29Makefile.build: a rule for building grammar.dotletouzey
2012-05-29Pfedit: two superfluous openletouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-05-29Makefile: avoid too much exported vars (for win32)letouzey
2012-05-25Bugs revealed by playing with contribspboutill
2012-05-25Fix r15259 to get rid of bug 2783pboutill
2012-05-25Fixed #2769.ppedrot
2012-05-25Fixed #2789.ppedrot
2012-05-23Rewritten the handling of coq sentence processing, hopefully beingppedrot
2012-05-23CHANGES: fix a typo + an entry in the wrong sectionletouzey
2012-05-23Fixed #2538 by adding an option to reset coqtop on tab switch, as suggested.ppedrot
2012-05-23Cleaned prerr_endline use.ppedrot
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
2012-05-23Fixed #2782.ppedrot
2012-05-23configure: camlp4 is now tried when camlp5 isn't foundletouzey
2012-05-23configure: add support of MinGW Win32 environment (fix #2526)letouzey
2012-05-23Reducing CoqIDE start option queries.ppedrot
2012-05-22Minilib: Always add the Coq_config.dirs to xdg_dirs (again)letouzey
2012-05-22Permutation: remove a compatibility notation which doesn't help MathClassesletouzey
2012-05-22SetoidList: explicit the fact that InfA_compat won't use ltA_strorderletouzey
2012-05-18List + Permutation : more results about nth_error and nthletouzey
2012-05-16Fixed bug #2781... (We hope so.)ppedrot
2012-05-16Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish.ppedrot
2012-05-16Coqide: make some paths win32-compliantletouzey
2012-05-16Revert commit 15287 : the env variables are indeed access at launch-timeletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-05-15Coqide: minor formatting improvement of an error messageletouzey
2012-05-15Coqide: in win32 command given to cmd.exe should be more quotedletouzey
2012-05-15when cross-compiling with mingw32, let's fix the Filename.dir_sepletouzey
2012-05-15Makefile: Really avoid locales in $(DATE)letouzey
2012-05-15Coqide: display initial connection errors in popups instead of on stderrletouzey
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-05-13Added semantic completion in CoqIDE. (Should also add an option for that...)ppedrot
2012-05-13Tweaking options of CoqIDE.ppedrot
2012-05-13Some cosmetic changes w.r.t. the previous commit.ppedrot
2012-05-13Heavily rewritten the coqtop management process of coqide. The coqtopppedrot
2012-05-13Added a SearchAbout-like primitive in coqtop interface.ppedrot
2012-05-13Added an interface primitive to ask coqtop for its internal versions.ppedrot
2012-05-11Vectors takes advantage of pattern matching compiler fixuppboutill
2012-05-11Impossible branches inference fixup (bug 2761)pboutill
2012-05-11Makefile.build typo in echopboutill
2012-05-11Slightly modified the coqtop interface by adding an identifier inppedrot
2012-05-11Tentative and very experminental support for typerex. Enabled withaspiwack
2012-05-11Coqide awful coqtop options parsing fixuppboutill