aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-05-30Getting rid of Pp.msgppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-30Restore compatibility with camlp4 (some missing open Tok)letouzey
2012-05-29Fixed an error display bug in CoqIDE.ppedrot
2012-05-29Re-allow Time Back* (cf discussion on coq-club)letouzey
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29Avoid Dumpglob dependency on Lexerletouzey
2012-05-29No need to have Refine amongst Hightactics.cm*aletouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Strongly reduce the dependencies of grammar.cma, modulo two hacksletouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
2012-05-29slim down a bit genarg.ml (pr_intro_pattern forgotten there)letouzey
2012-05-29Glob_term: minor formattingletouzey
2012-05-29Migrate the grammar entry about "Ltac" into g_vernac.ml4.letouzey
2012-05-29simplification in deps of some g_*.ml4letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
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