aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-12-17Fixing format of complexity bug Notations.v.herbelin
2011-12-16Fixing previous commit which was bugging on tactics preceded by goal number (...courtieu
2011-12-16Coqide: adapt some comments now that bullets are terminators like { }letouzey
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
2011-12-16Adapting coqide to my last commit: courtieu
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...ppedrot
2011-12-14Some extra universe refreshing seems needed in abstract_generalizeherbelin
2011-12-12CHANGES: some more updatesletouzey
2011-12-12Proof using ...gareuselesinge
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
2011-12-08Makefile: force the installation of all .cmi (and remove some obsolete .mli)letouzey
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-07Html page titlespboutill
2011-12-07Vectors use a bit more the pattern matching compilerpboutill
2011-12-07Typopboutill
2011-12-06Fixed a synchronization bug between coqtop and the CoqIDE command pane.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:21:31 +0000