| Age | Commit message (Expand) | Author |
|---|
| 2011-04-21 | Win32: remove the need for Coq.bat and Coqide.bat | letouzey |
| 2011-04-21 | Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ... | letouzey |
| 2011-04-21 | Ocamlbuild: in win32, coqide is now a console-free app by default | letouzey |
| 2011-04-21 | Win32: let's directly make coqtop.exe and coqide.exe incorporate coq.ico | letouzey |
| 2011-04-21 | bug fix: concurrent access of persistent_cache | fbesson |
| 2011-04-20 | Coqide: Fix the command separator for external cmds (#2363) | letouzey |
| 2011-04-20 | Coqdoc: also try coqlib relative to the coqdoc binary location | letouzey |
| 2011-04-20 | Allow betaiota when checking unification of the types of metas (fixes ATBR co... | msozeau |
| 2011-04-20 | Don't force progress on instance applications, there is always progress when ... | msozeau |
| 2011-04-20 | This is used in the rippling plugin. This also allows fixing bug #2188. | msozeau |
| 2011-04-19 | Declarative mode: fix escape and return. | aspiwack |
| 2011-04-19 | Fix thumb2-related build error | glondu |
| 2011-04-18 | Fix generated script for NMake, a rewrite necessitates full conversion for | msozeau |
| 2011-04-18 | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau |
| 2011-04-16 | Fix unification of types of metavariables and error message for sort unificat... | msozeau |
| 2011-04-15 | Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x". | herbelin |
| 2011-04-15 | Coqc: fix the exit code | letouzey |
| 2011-04-15 | Extraction: nicer error when a toplevel module has no body (#2525) | letouzey |
| 2011-04-15 | Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515) | letouzey |
| 2011-04-15 | Documentation typo. | gmelquio |
| 2011-04-14 | More informative anomaly. | herbelin |
| 2011-04-14 | Add directories in COQPATH to search path. | herbelin |
| 2011-04-14 | Reorder search path order, so the standard library is search last. | herbelin |
| 2011-04-13 | Extraction: opaque terms are not traversed anymore by default | letouzey |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Put dependent subgoals first so as to allow backtracking on them, might chang... | msozeau |
| 2011-04-13 | - Make typeclass transparency information directly available | msozeau |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-04-13 | Fix merge. | msozeau |
| 2011-04-13 | - Improve unification (beta-reduction, and same heuristic as evarconv for red... | msozeau |
| 2011-04-13 | Fix scripts relying on unification not doing any beta reduction. | msozeau |
| 2011-04-13 | Unify meta types with the right flags, add betaiotazeta reduction to unificat... | msozeau |
| 2011-04-13 | Proper typing of metavariables, type errors were completely ignored before...... | msozeau |
| 2011-04-13 | - Do not make constants with an assigned type polymorphic (wrong unfoldings). | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-12 | Subtyping: align coqtop behavior concerning opaque csts on coqchk's one | letouzey |
| 2011-04-12 | remove old traces of SearchIsos (never ported to 7.x nor 8.x) | letouzey |
| 2011-04-11 | Catch NotArity exception and transform it into an anomaly in retyping. | msozeau |
| 2011-04-08 | ocamlbuild: support again camlp5 in addition to camlp4 | letouzey |
| 2011-04-08 | Applying Tom Prince's patch to coqdep not correctly applying the -R visibility | herbelin |
| 2011-04-08 | A kind of reply to bug 2444 | pboutill |
| 2011-04-08 | weak dependency of coqtop for coqide and coqc (bug 2390) | pboutill |
| 2011-04-08 | A 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-08 | Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395 | pboutill |
| 2011-04-08 | More up to date About in coqide | pboutill |
| 2011-04-08 | Macos integration step2 : shutdown | pboutill |
| 2011-04-08 | coqide shutdown process change (and out the main function) | pboutill |
| 2011-04-08 | Applying Tom Prince's patch for build_constant_by_tactic not able to | herbelin |
| 2011-04-08 | Made warning about ending comments in string less intrusive so as to support | herbelin |
