| Commit message (Expand) | Author | Age |
|---|
| * | 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-31 |
| * | 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-30 |
| * | 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-28 |
| * | 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-25 |
| * | 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-23 |
| * | 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-21 |
| * | 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-18 |
| * | 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-17 |
| * | 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-16 |
| * | 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-13 |
| * | 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-11 |
| * | 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-10 |
| * | 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-08 |
| * | 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 |
herbelin
glondu
letouzey
msozeau
pottier
bgregoir