coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	New module Xml_printer (dual to Xml_parser)	gareuselesinge	2013-05-06
*	Coqide: view -> zoom in / out / fit	gareuselesinge	2013-05-06
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Summary: support selective freeze	gareuselesinge	2013-05-06
*	Ideutils: comment on missing Glib utf8 handling function	gareuselesinge	2013-05-06
*	Close the .glob file after having saved .vo	gareuselesinge	2013-05-06
*	Fix typo in manual	gareuselesinge	2013-05-06
*	Improving printing of 'rew' notation	herbelin	2013-05-05
*	Hack to solve a "Bad recursive type" anomaly.	herbelin	2013-05-05
*	Now printing body of abbreviations (i.e. notation with a name) with	herbelin	2013-05-05
*	Little fix for Nsatz: hypotheses not directly relevant to the nsatz	herbelin	2013-05-05
*	Improvement of r16204 on reporting tactic error locations: if the main	herbelin	2013-05-05
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Reporting the change on matching partial applications in patterns of	herbelin	2013-05-05
*	Removing a redundant function from Evd.	ppedrot	2013-05-03
*	Fix wrong computation of dependency signature in cases raising an uncaught ex...	msozeau	2013-04-30
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Added a unit test for bug #2230.	ppedrot	2013-04-27
*	Fix compilation (vernac.ml, missing ;)	gareuselesinge	2013-04-25
*	Fix: tooltip correctly handles the absence of info (empty string)	gareuselesinge	2013-04-25
*	Coqide: Globalization feedback (proof of concept)	gareuselesinge	2013-04-25
*	lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutils	gareuselesinge	2013-04-25
*	Flag ide_slave moved into Flags module	gareuselesinge	2013-04-25
*	Coqide: new tag "tooltip" for the Script window	gareuselesinge	2013-04-25
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Coqide: new feedback mechanism for structured content	gareuselesinge	2013-04-25
*	Fix indentation	gareuselesinge	2013-04-25
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	Egramcoq+Lexer : no need for an init_function	letouzey	2013-04-23
*	Indfun : use States.with_state_protection instead of freeze/unfreeze	letouzey	2013-04-23
*	Egramcoq: clean an ugly code snippet	letouzey	2013-04-23
*	minor cleanup in coqtop.ml	letouzey	2013-04-23
*	coqtop -compile: avoid with_heavy_rollback when non-interactive	letouzey	2013-04-23
*	Coqtop -compile : avoid saving init state when compiling just one file	letouzey	2013-04-23
*	Remove deprecated option -no-hash-consing (currently doing nothing)	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Declaremods: some more minor cleanup	letouzey	2013-04-22
*	Fix compilation of fake_ide	gareuselesinge	2013-04-19
*	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge	2013-04-19
*	coqc and coqmktop migrated in tools/, get rid of scripts/ subdir	letouzey	2013-04-18
*	Coqdep: add an -exclude-dir option (wish mentionned in #3025)	letouzey	2013-04-18
*	Coqc: accept -exclude-dir + some others + cleanup (fix #3025)	letouzey	2013-04-18
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Only arguments declared as implicit can be renamed	gareuselesinge	2013-04-18
*	Fix #3001 (rename arg of global cst inside section)	gareuselesinge	2013-04-18
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Fix of r16257 in r16205 for "errors raised by check_evar_instance were	herbelin	2013-04-17
*	Coqmktop: dynlink is now mandatory due to Maxime's native-compiler	letouzey	2013-04-17