coq - The formal proof system

Age	Commit message (Expand)	Author
2011-03-30	Ide_intf: remove useless int answer to the "interp" and "rewind" calls	letouzey
2011-03-30	Ide_slave: better handling of Ctrl-C	letouzey
2011-03-30	Coqide: synchronise the reset_initial via the coq_computing mutex	letouzey
2011-03-28	Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_break	letouzey
2011-03-28	Ide: restaure compilation of ide/macjokes.c removed by mistake	letouzey
2011-03-28	Ide: misc (nicer message than End_of_file, a useless try removed	letouzey
2011-03-28	Ide_slave: improved handling of exceptions (in particular ^C)	letouzey
2011-03-28	Ide_slave: a more robust current_status () function	letouzey
2011-03-28	Ide: new option -coqtop <mycoqtop> + remove wrong quoting of args	letouzey
2011-03-25	ide/coqide.ml: a pass of more decent automatic indentation	letouzey
2011-03-25	Ide: more reorganisation and cleanup	letouzey
2011-03-25	Ide_intf : change type of location in ide	letouzey
2011-03-25	Ide: mention "Restart" instead of "Go to start" for corresponding button	letouzey
2011-03-23	Ide: stronger separation from coqtop	letouzey
2011-03-23	Ide: experimentally allow coqide to interrupt or kill coqtop	letouzey
2011-03-23	- Remove useless grammar rule	msozeau
2011-03-23	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau
2011-03-21	Documentation of the timeout tactical (cf r13917)	letouzey
2011-03-21	Init: some results in Type should rather be Defined than Qed	letouzey
2011-03-21	Makefile.build: states/initial.coq was wrongly done with -dont-load-proofs	letouzey
2011-03-18	Makefile.build: compile the stdlib with -dont-load-proofs by default	letouzey
2011-03-18	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey
2011-03-17	An option "Set Default Timeout n."	letouzey
2011-03-17	Goptions: repair Unset for int options	letouzey
2011-03-17	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey
2011-03-16	Adapt printers.mllib after my last commit	letouzey
2011-03-16	Finish branching functions handling module errors (cf. r13886)	letouzey
2011-03-16	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey
2011-03-16	Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction	letouzey
2011-03-13	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-11	Keep information on which fields are subclasses in class declarations,	msozeau
2011-03-11	Inference of match predicate produces ill-typed unification problem,	msozeau
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-11	- Better error messages taking unif. constraints into account.	msozeau
2011-03-10	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau
2011-03-10	Do not forget conv_pbs when resetting an evm:	msozeau
2011-03-10	ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditions	letouzey
2011-03-08	Solve evar instantiations in the right environment.	msozeau
2011-03-08	Fix declarations of [Add Setoid/Morphism...] in sections to not export	msozeau
2011-03-08	syntax for exponents	pottier
2011-03-08	adding eta in the vm	bgregoir
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Revert commit r13883: instantiating ?n by a lambda when "?n a" has to	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-03-07	CHANGES: mentionning quickly Separate Extraction	letouzey
2011-03-07	Extraction: a warning when an opaque constant is enterred	letouzey
2011-03-07	Extraction: fix printing of haskell modular names	letouzey
2011-03-07	Extraction: avoid printing unused mutual fix components (fix #2477)	letouzey
2011-03-07	A new command "Separate Extraction"	letouzey