aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-01-07Fix typoglondu
2012-01-06Fixed the itarget of the previous commit...ppedrot
2012-01-06Added a typeclass-based system to reason on decidable propositions.ppedrot
2012-01-06Forbids (as it has always been the behaviour) to have two different openaspiwack
2012-01-06Fixes bug #2654 (tactic instantiate failing to update existential variables).aspiwack
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2012-01-03Makefile.doc: attempt to solve race condition for creating doc/refman/html.herbelin
2011-12-27Bug 2669 and more: make full-stdlibpboutill
2011-12-26Coqdoc: Fixing missing newline when using "Proof term."herbelin
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
2011-12-26update CHANGES w.r.t. simplgareuselesinge
2011-12-25Version number, copyright, credits: missing updates.herbelin
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
2011-12-23myocamlbuild: -DWIN32 instead of -DWin32letouzey
2011-12-23Configure: the backslashes in win32 paths should be escapedletouzey
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
2011-12-21sequel of previous commitletouzey
2011-12-21Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...letouzey
2011-12-21Pure interfaces shouldn't be mentionned in .mllibletouzey
2011-12-21adapt myocamlbuild after changes in coqdep_boot (.beautify)letouzey
2011-12-21Cleaning CHANGES file.herbelin
2011-12-19Notifying removal of accidental unfolding of recursive calls ofherbelin
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
2011-12-19test suite update after r14808pboutill
2011-12-19Bug 2377 part 2: old revision file is erased by installpboutill
2011-12-19Fixed some printing details for dependent evars in emacs mode. Patchcourtieu
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-12-18CoqIde files position is freedesktop compliant.pboutill
2011-12-18./configure & freedesktoppboutill
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
2011-12-18Applied patches proposed suggested by Hendrik Tews to fix existentialcourtieu
2011-12-18Continuing 14812 and 14813 (use type information to reduce theherbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-18Removing PrintConstr debugging entry in g_proof.ml4 which was notherbelin
2011-12-18Suspending declaration of undefined debug printers.herbelin
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-17Reorganizing Unification.unify_0 so as to more easily share codeherbelin
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-17Coq_makefile: "beautify" targetpboutill
2011-12-17Coqdep adds %.v.beautified on the left of the ':' when it generates %.v depen...pboutill
2011-12-17Coq_makefile: "validate" target calls the checker over all vo.pboutill
2011-12-17Coq_makefile: section refactoring and no variables for OCaml if no ml* files ...pboutill
2011-12-17Coq_makefile: if no -install is provided, install location is set by a Makefi...pboutill
2011-12-17Deactivated automatic inference of _case schemes, as it was in 8.3herbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
2011-12-17Improving pretty-printing of Ltac functions.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:52:45 +0000