aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-22Correction of error message (bug 3359)Julien Forest
2014-09-22Fixing bug 3951Julien Forest
2014-09-21Rewrite.apply_lemma is written in state passing style.Pierre-Marie Pédrot
2014-09-21More invariants in the code of Refine.Pierre-Marie Pédrot
2014-09-21Removing a nonsensical Errors.push.Pierre-Marie Pédrot
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
2014-09-19Use smart mapping in map_constr_with_binders_left_to_right.Matthieu Sozeau
2014-09-19Fixing bug #3646.Pierre-Marie Pédrot
2014-09-19win32: embed NSIS for plugin writersEnrico Tassi
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2014-09-19Revert change of e_contextually as it needlessly expands all primitiveMatthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-18Do not try to match on a subterm that is not closed in find_subterm.Matthieu Sozeau
2014-09-18Clean a bit of univ.ml, add credits.Matthieu Sozeau
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-18For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...Hugo Herbelin
2014-09-18mltop: when a plugin is loaded store its full path in the summaryEnrico Tassi
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-18fix coq_makefilePierre Boutillier
2014-09-18configure.ml: opam camlp5 + system ocaml worksPierre Boutillier
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-17Change some Defined into Qed.Guillaume Melquiond
2014-09-17Add some missing Proof statements.Guillaume Melquiond
2014-09-17Remove pointless regex for '""' as the empty string already matches it.Guillaume Melquiond
2014-09-17Revert "coqc: execvp is now available even on win32"Enrico Tassi
2014-09-17win32: remove outdated splash screenEnrico Tassi
2014-09-17Fix highlighting of "Hint Unfold" and "Hint Rewrite".Guillaume Melquiond
2014-09-17Properly highlight the Export keyword.Guillaume Melquiond
2014-09-17Fix ambiguous regex in syntax highlighting.Guillaume Melquiond
2014-09-17Change an axiom into a definition.Guillaume Melquiond
2014-09-17Fix broken syntax highlighting for Coq files using "Proof constr".Guillaume Melquiond
2014-09-17win32: bring back the coq icon in the coqide binaryEnrico Tassi
2014-09-17win32: use subsystem windows on windows (and not console)Enrico Tassi
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Matthieu Sozeau
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
2014-09-17Update test-suite files after last commit. Add a file for rewrite_stratMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-16better error messageEnrico Tassi
2014-09-16fix test-suite/success/decl_mode.vEnrico Tassi
2014-09-16More on printing references applied to implicit arguments.Hugo Herbelin
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Adapting ltac output test to new interpretation of binders.Hugo Herbelin
2014-09-15Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Hugo Herbelin
2014-09-15Not printing goal name (reinstalled by mistake in a previous commit).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 03:56:12 +0000