aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-12-14CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' messageEnrico Tassi
2015-12-14Updating CHANGES with an incompatibility.Hugo Herbelin
2015-12-14Revert PMP's fix of #2498, which introduces an incompatibility with lablgtkMaxime Dénès
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-14Test file for #4363 was not complete.Maxime Dénès
2015-12-14Extraction: cosmetically avoid generating spaces on empty linesPierre Letouzey
2015-12-14Extraction: also get rid of explicit '\n' for haskellPierre Letouzey
2015-12-14Extraction: fix a pretty-print issuePierre Letouzey
2015-12-14Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Pierre Letouzey
2015-12-12Extraction: documentation of the new option Unset Extraction SafeImplicitsPierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-12-12Extraction: check for remaining implicits after dead code removal (fix #4243)Pierre Letouzey
2015-12-12Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Pierre Letouzey
2015-12-12Extraction: avoid generating some blanks at end-of-linePierre Letouzey
2015-12-12Indexing and documenting some options.Pierre-Marie Pédrot
2015-12-11Optimize occur_evar_upto_types, avoiding repeateadly looking into theMatthieu Sozeau
2015-12-11Univs: Fix bug #4363, nested abstract.Matthieu Sozeau
2015-12-11Document removal of Set Virtual Machine and -vm in CHANGES.Maxime Dénès
2015-12-11Remove Set Virtual Machine from doc, since the command itself has been removed.Maxime Dénès
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-10Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removingHugo Herbelin
2015-12-10Silently ignore requests to _not_ clear something when that something cannot ...Guillaume Melquiond
2015-12-10Refman, ch. 4: A few fixes.Hugo Herbelin
2015-12-10ENH: redundant examples were removedMatej Kosik
2015-12-10FIX: wrong reference to a figureMatej Kosik
2015-12-10CLEANUP: putting examples inside "figure" environmentMatej Kosik
2015-12-10ENH: The definition of the "_ ; _" operation on local context was added.Matej Kosik
2015-12-10TYPOGRAPHY: adjustmentsMatej Kosik
2015-12-10PROPOSITION: the side-condition was made more specific.Matej Kosik
2015-12-10PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Matej Kosik
2015-12-10PROPOSITION: Added an explicit definition of the notation for enriching the g...Matej Kosik
2015-12-10PROPOSITION: Added "if" and "then" words missing in the original sentence.Matej Kosik
2015-12-10PROPOSITION: Example was simplifiedMatej Kosik
2015-12-10DONEMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10GRAMMAR: added punctuationMatej Kosik
2015-12-10CLEANUP PROPOSITION: rephrasing the original idea in a simpler wayMatej Kosik
2015-12-10CLEANUP PROPOSITION: existing example was removed because it is not urgently ...Matej Kosik
2015-12-10ENH: existing example was changed so that it is now linked to the results sho...Matej Kosik
2015-12-10ENH: an existing example was further expanded.Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 14:42:52 +0000