aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
2011-04-21Win32: remove the need for Coq.bat and Coqide.batletouzey
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-11An generic imperative union-find, used for deps of evars in Class_tacticsletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
2011-01-06Remove Safe_marshalglondu
2010-12-25Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsglondu
2010-12-06Use !Pp_control.std_ft for printing grammarsglondu
2010-12-03Remove dead codeglondu
2010-11-18adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6letouzey
2010-11-16Support for camlp5 6.02.0 (Closes: #2432)glondu
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
2010-09-17Coqdep_boot : misc improvementsletouzey
2010-08-31* By default, load proof terms.regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
2010-07-29Fixed a bug introduced (r13316/r13329) in the printing of notationsherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-07-20Fixed a bug in list_forall2eq (wrong exception was caught).herbelin
2010-07-02Remove dependency to Unix from module Profileglondu
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix #2158...letouzey
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-06-01restore handling of lexer errorsletouzey
2010-05-31CoqIDE goes multiprocessvgross
2010-05-28Account for Stephane Glondu's remarks.fkirchne
2010-05-28Use existing functions to reimplement search_exe.fkirchne
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayletouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-27Added a new exception for already declared Schemes, vsiles
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin