aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-12Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneletouzey
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
2011-04-08ocamlbuild: support again camlp5 in addition to camlp4letouzey
2011-04-08Applying Tom Prince's patch to coqdep not correctly applying the -R visibilityherbelin
2011-04-08A kind of reply to bug 2444pboutill
2011-04-08weak dependency of coqtop for coqide and coqc (bug 2390)pboutill
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
2011-04-08@ in index of refman (last request of bug 2494)pboutill
2011-04-08Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395pboutill
2011-04-08More up to date About in coqidepboutill
2011-04-08Macos integration step2 : shutdownpboutill
2011-04-08coqide shutdown process change (and out the main function)pboutill
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
2011-04-08Made warning about ending comments in string less intrusive so as to supportherbelin
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
2011-04-08Fixed "Eval ... in t" when t has still metavariables.herbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-04-07Extraction: unfolds the let-in created by Program when handling "match"letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 22:17:26 +0000