| Age | Commit message (Expand) | Author |
|---|
| 2011-04-03 | Quickly avoid global axioms in Loic new files about ring | letouzey |
| 2011-04-01 | Adjust coqdep so that it behaves like coqtop with respect to the user-contrib... | gmelquio |
| 2011-04-01 | CHANGES: a word about recent changes in coqide, about Ctrl-C in vm | letouzey |
| 2011-04-01 | Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental) | letouzey |
| 2011-03-31 | Did that adding a rule for printing applications as "f(x)" works. | herbelin |
| 2011-03-31 | As remarked by Enrico, we'd better use eq_constr than structural equality | herbelin |
| 2011-03-31 | Extraction: customized inductives are always standard | glondu |
| 2011-03-30 | Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin) | letouzey |
| 2011-03-30 | Coqide: avoid confusion of process when restarting coqtop + cosmetic | letouzey |
| 2011-03-30 | Ide_intf: documentation of calls + debug printing of calls/answers | letouzey |
| 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 |
