aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix scripts relying on unification not doing any beta reduction.Gravatar msozeau2011-04-13
* Unify meta types with the right flags, add betaiotazeta reduction to unificat...Gravatar msozeau2011-04-13
* Proper typing of metavariables, type errors were completely ignored before......Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
* remove old traces of SearchIsos (never ported to 7.x nor 8.x)Gravatar letouzey2011-04-12
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
* ocamlbuild: support again camlp5 in addition to camlp4Gravatar letouzey2011-04-08
* Applying Tom Prince's patch to coqdep not correctly applying the -R visibilityGravatar herbelin2011-04-08
* A kind of reply to bug 2444Gravatar pboutill2011-04-08
* weak dependency of coqtop for coqide and coqc (bug 2390)Gravatar pboutill2011-04-08
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
* Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395Gravatar pboutill2011-04-08
* More up to date About in coqideGravatar pboutill2011-04-08
* Macos integration step2 : shutdownGravatar pboutill2011-04-08
* coqide shutdown process change (and out the main function)Gravatar pboutill2011-04-08
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
* Made warning about ending comments in string less intrusive so as to supportGravatar herbelin2011-04-08
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* Fixed "Eval ... in t" when t has still metavariables.Gravatar herbelin2011-04-08
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
* Extraction: unfolds the let-in created by Program when handling "match"Gravatar letouzey2011-04-07
* Extraction: avoid some useless Obj.magic by fixing my ML type unifierGravatar letouzey2011-04-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:41:59 +0000