aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-05-16Put the "change" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "specialize_eq" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize dependent" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "*_cast_no_check" tactics in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact_constr" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-16Fix bug #4737: cycle tactic doesn't like zero goals.Pierre-Marie Pédrot
2016-05-16Generate more user-readable tactic notation kernel names.Pierre-Marie Pédrot
2016-05-16Merge pull request #170 from relrod/patch-1Pierre-Marie Pédrot
2016-05-15Fix a really small doc typoRicky Elrod
2016-05-14Removing unexcepted activation of option "Regular Subst Tactic", sinceHugo Herbelin
2016-05-14More hints on how to fix compatibility issues.Hugo Herbelin
2016-05-14Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.Pierre-Marie Pédrot
2016-05-13Dyn: simplify API introducing an Easy submoduleEnrico Tassi
2016-05-13More informative error message when interpreting ltac variables in terms.Pierre-Marie Pédrot
2016-05-12Small optimization in evar resolution.Pierre-Marie Pédrot
2016-05-12Fix bug #4722: Coq dies when encountering broken symbolic links.Pierre-Marie Pédrot
2016-05-11Thorough rewriting of the Pcoq API towards safety and static invariants.Pierre-Marie Pédrot
2016-05-11The grammar_extend function now registers unsynchronized extensions.Pierre-Marie Pédrot
2016-05-11Making the grammar command extend API purely functional.Pierre-Marie Pédrot
2016-05-11Moving the constr empty entry registering to the state-based API.Pierre-Marie Pédrot
2016-05-11Turning the grammar extend command API into a state-passing one.Pierre-Marie Pédrot
2016-05-11Moving the grammar summary to Pcoq.Pierre-Marie Pédrot
2016-05-10Delimiting the use of unsafe code in Pcoq.Pierre-Marie Pédrot
2016-05-10Overlooked use of Gram instead of G module in Pcoq.Pierre-Marie Pédrot
2016-05-10Further tidying of the constr extension code.Pierre-Marie Pédrot
2016-05-10Type-safe constr notations.Pierre-Marie Pédrot
2016-05-10AlistNsep token now accepts an arbitrary separator.Pierre-Marie Pédrot
2016-05-10Simpler data structure for Arules token.Pierre-Marie Pédrot
2016-05-10Purer implementation of empty level registering in Pcoq.Pierre-Marie Pédrot
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-10Hardening the obsolete unsafe_grammar_statement API.Pierre-Marie Pédrot
2016-05-10Removing dead code in Compat.Pierre-Marie Pédrot
2016-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-05-10STM: code cleanupEnrico Tassi
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-09Fix bug #3887: Better error message for "More than one program with unsolved ...Pierre-Marie Pédrot
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-05-09Fix typo in configure's option description.Guillaume Melquiond
2016-05-09Use "md5 -q" on FreeBSD architectures (bug #4719).Guillaume Melquiond
2016-05-09Use the actual location of an error in the error pane (bug #4169).Guillaume Melquiond
2016-05-08Exposing structure of the entries to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Actually using the symbol information to print Tactic Notations properly.Pierre-Marie Pédrot
2016-05-08Removing dead code in Pptactic.Pierre-Marie Pédrot
2016-05-08Pass user symbol to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:10:45 +0000