aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2011-07-29Refl_omega: replaced some generic = on constr by eq_constrpuech
2011-07-29Coq_omega: replaced generic = on constr by eq_constrpuech
2011-07-29Hahtbl_alt: separate generic combine functionspuech
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
2011-07-29Term: Refactoring of hashconsingpuech
2011-07-22For the beauty of tail recursion, a new list_addnpboutill
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-19Remove useless "open Gc"glondu
2011-05-19Remove System.process_time (dead code)glondu
2011-05-17More work on error handlingletouzey
2011-05-13A new mechanism to handle errors.aspiwack
2011-04-29Choose relative directory over configured directory for coqlib.pboutill
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 14:52:47 +0000