aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-04-07Extraction: avoid some useless Obj.magic by fixing my ML type unifierletouzey
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
2011-04-06Fix dev/base_include after change of constant_bodyletouzey
2011-04-06Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.aspiwack
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
2011-04-03Fix last commit about coqdep: not everyone has a user-contrib dirletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-04-03Quickly avoid global axioms in Loic new files about ringletouzey
2011-04-01Adjust coqdep so that it behaves like coqtop with respect to the user-contrib...gmelquio
2011-04-01CHANGES: a word about recent changes in coqide, about Ctrl-C in vmletouzey
2011-04-01Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)letouzey
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-31As remarked by Enrico, we'd better use eq_constr than structural equalityherbelin
2011-03-31Extraction: customized inductives are always standardglondu
2011-03-30Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)letouzey
2011-03-30Coqide: avoid confusion of process when restarting coqtop + cosmeticletouzey
2011-03-30Ide_intf: documentation of calls + debug printing of calls/answersletouzey
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
2011-03-30Coqide: synchronise the reset_initial via the coq_computing mutexletouzey
2011-03-28Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakletouzey
2011-03-28Ide: restaure compilation of ide/macjokes.c removed by mistakeletouzey
2011-03-28Ide: misc (nicer message than End_of_file, a useless try removedletouzey
2011-03-28Ide_slave: improved handling of exceptions (in particular ^C)letouzey
2011-03-28Ide_slave: a more robust current_status () functionletouzey
2011-03-28Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsletouzey
2011-03-25ide/coqide.ml: a pass of more decent automatic indentationletouzey
2011-03-25Ide: more reorganisation and cleanupletouzey
2011-03-25Ide_intf : change type of location in ideletouzey
2011-03-25Ide: mention "Restart" instead of "Go to start" for corresponding buttonletouzey
2011-03-23Ide: stronger separation from coqtopletouzey
2011-03-23Ide: experimentally allow coqide to interrupt or kill coqtopletouzey
2011-03-23- Remove useless grammar rulemsozeau
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...msozeau
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-21Init: some results in Type should rather be Defined than Qedletouzey
2011-03-21Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsletouzey
2011-03-18Makefile.build: compile the stdlib with -dont-load-proofs by defaultletouzey
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-17An option "Set Default Timeout n."letouzey
2011-03-17Goptions: repair Unset for int optionsletouzey
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-03-16Adapt printers.mllib after my last commitletouzey
2011-03-16Finish branching functions handling module errors (cf. r13886)letouzey
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 06:18:24 +0000