aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Unicode.ascii_of_ident is now truly injectivePierre Letouzey
2016-05-19Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Pierre Letouzey
2016-05-17Putting all the tactics exported by the Tactics module in the new monad API.Pierre-Marie Pédrot
2016-05-17Removing some compatibility layers in Tactics.Pierre-Marie Pédrot
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
2016-05-17Put the "move" tactic in the monad.Pierre-Marie Pédrot
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 14:51:03 +0000