aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
* Fix dev/base_include after change of constant_bodyGravatar letouzey2011-04-06
* Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.Gravatar aspiwack2011-04-06
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
* Fix last commit about coqdep: not everyone has a user-contrib dirGravatar letouzey2011-04-03
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Quickly avoid global axioms in Loic new files about ringGravatar letouzey2011-04-03
* Adjust coqdep so that it behaves like coqtop with respect to the user-contrib...Gravatar gmelquio2011-04-01
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
* As remarked by Enrico, we'd better use eq_constr than structural equalityGravatar herbelin2011-03-31
* Extraction: customized inductives are always standardGravatar glondu2011-03-31
* Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)Gravatar letouzey2011-03-30
* Coqide: avoid confusion of process when restarting coqtop + cosmeticGravatar letouzey2011-03-30
* Ide_intf: documentation of calls + debug printing of calls/answersGravatar letouzey2011-03-30
* Ide_intf: remove useless int answer to the "interp" and "rewind" callsGravatar letouzey2011-03-30
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
* Coqide: synchronise the reset_initial via the coq_computing mutexGravatar letouzey2011-03-30
* Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakGravatar letouzey2011-03-28
* Ide: restaure compilation of ide/macjokes.c removed by mistakeGravatar letouzey2011-03-28
* Ide: misc (nicer message than End_of_file, a useless try removedGravatar letouzey2011-03-28
* Ide_slave: improved handling of exceptions (in particular ^C)Gravatar letouzey2011-03-28
* Ide_slave: a more robust current_status () functionGravatar letouzey2011-03-28
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
* ide/coqide.ml: a pass of more decent automatic indentationGravatar letouzey2011-03-25
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
* Ide: mention "Restart" instead of "Go to start" for corresponding buttonGravatar letouzey2011-03-25
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
* - Remove useless grammar ruleGravatar msozeau2011-03-23
* - Fix solve_simpl_eqn which was cheking instances types in the wrong environm...Gravatar msozeau2011-03-23
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
* Init: some results in Type should rather be Defined than QedGravatar letouzey2011-03-21
* Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsGravatar letouzey2011-03-21
* Makefile.build: compile the stdlib with -dont-load-proofs by defaultGravatar letouzey2011-03-18
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Adapt printers.mllib after my last commitGravatar letouzey2011-03-16
* Finish branching functions handling module errors (cf. r13886)Gravatar letouzey2011-03-16
* Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)Gravatar letouzey2011-03-16
* Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionGravatar letouzey2011-03-16
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:07:12 +0000