aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-07-07Ring_polynom : a restricted simpl instead of a unfold;foldletouzey
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
2012-07-06Two adaptations after the changes of level of ->letouzey
2012-07-06BinPos/BinInt/BinNat : fix some argument scopesletouzey
2012-07-06Restore the compatibility notation Compare.not_eq_symletouzey
2012-07-06Fix order of introduction of hints to preserve most-recent-first semantics.msozeau
2012-07-06A prototype implementation of a Print Namespace command.aspiwack
2012-07-06Fixes a bug in the parsing of the grammar entry dirpath which would,aspiwack
2012-07-06Practical fix for bug #1206 (anomaly raised in pretyping instead ofherbelin
2012-07-06Fixes bug #2678aspiwack
2012-07-06Backtrack: add support for the "Proof c." syntax (fix #2832)letouzey
2012-07-05Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)letouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Quick update to CHANGES, mention especially the new parsing of ->letouzey
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
2012-07-05More cleanup in Ring_polynom and EnvRingletouzey
2012-07-05Some cleanup in recent proofs concerning piletouzey
2012-07-05MSetRBT : elementary arith proofs instead of calls to lialetouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05Open Scope can now also accepts delimiters (e.g. Z).letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-07-05Fixes in rewriting by strategies (almost ready to be documented!):msozeau
2012-07-04Fixes a bug in Ppvernac which had braces and bullets printed with an endingaspiwack
2012-07-04Change how the number of open goals is printed.aspiwack
2012-07-04When focused on an empty list of goal (after finishing a subproof introducedaspiwack
2012-06-29Various small display improvementppedrot
2012-06-29Reversed message display order in CoqIDEppedrot
2012-06-29Small improvement to ide_slave, which was going crazy wheneverppedrot
2012-06-29Fixing fake_ideppedrot
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
2012-06-28Cleaning opening of the standard List module.ppedrot
2012-06-28Replace nat indices with positive one in Btauto.ppedrot
2012-06-28Fixing previous commit.ppedrot
2012-06-28Fixing info_auto / info_trivial display.ppedrot
2012-06-26Added the show_margin_right option to CoqIDEppedrot
2012-06-26Fixing awkward copy & paste mechanism in CoqIDE.ppedrot
2012-06-26Now CoqIDE auto-sets the printing width of the goal display.ppedrot
2012-06-26Fixed string width printing in string_of_ppcmdsppedrot
2012-06-26Added a Deque module to CLib (to be used in CoqIDE).ppedrot
2012-06-25Small code compaction and factoring in CoqIDE.ppedrot
2012-06-25Added a .mli to pretyping/program.mlppedrot
2012-06-24Cosmetic changesppedrot
2012-06-24Made the message view of CoqIDE abstract.ppedrot
2012-06-23Documentation of pp.mlippedrot
2012-06-23Moving logging level to Interface.ppedrot
2012-06-23Fixed cursor reset in CoqIDE backtrack.ppedrot
2012-06-23Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 13:44:07 +0000