aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-09-15Fixing line break in test for #3559.Hugo Herbelin
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
2014-09-15Ltac names in binders: some Ltac values can be seen both as terms and identif...Arnaud Spiwack
2014-09-15Fix: when interpreting a identifier in pretying, use the Ltac identifier subs...Arnaud Spiwack
2014-09-15Fix a bug in the naming of binders.Arnaud Spiwack
2014-09-15A small pass of code cleaning and clenv removing in Rewrite.Pierre-Marie Pédrot
2014-09-15Fixing bug #3619 in emacs mode.Hugo Herbelin
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
2014-09-15Fix bug #3610, allowing betaiotadelta reduction while unifying types ofMatthieu Sozeau
2014-09-15Fix bug #3621, using fold_left2 on arrays of the same size only.Matthieu Sozeau
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-15Removing one Evd.merge in Rewrite.Pierre-Marie Pédrot
2014-09-15More invariants in Rewrite unification.Pierre-Marie Pédrot
2014-09-15The unifying functions of Rewrite uses the return types of strategies.Pierre-Marie Pédrot
2014-09-15Splitting the uses of the unification function according to the status ofPierre-Marie Pédrot
2014-09-14Rewrite.apply_strategy uses the same return type as strategies.Pierre-Marie Pédrot
2014-09-14Proper type for rewrite strategy results.Pierre-Marie Pédrot
2014-09-13Prepare goal name printing but no not print them at the current time.Hugo Herbelin
2014-09-13Using "Evd.restrict" in tactic clear so as to keep evar names.Hugo Herbelin
2014-09-13Exporting apply_subfilter from Evd.ml.Hugo Herbelin
2014-09-13Retroknowledge arguments are made VERNAC ARGUMENTS.Pierre-Marie Pédrot
2014-09-13Fixing synchronization of evar names table when merging evar_map.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 16:10:55 +0000