| Age | Commit message (Expand) | Author |
|---|
| 2014-09-18 | Do not try to match on a subterm that is not closed in find_subterm. | Matthieu Sozeau |
| 2014-09-18 | Clean a bit of univ.ml, add credits. | Matthieu Sozeau |
| 2014-09-18 | Fixing strange evarmap leak in goals. | Pierre-Marie Pédrot |
| 2014-09-18 | For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ... | Hugo Herbelin |
| 2014-09-18 | mltop: when a plugin is loaded store its full path in the summary | Enrico Tassi |
| 2014-09-18 | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier |
| 2014-09-18 | fix coq_makefile | Pierre Boutillier |
| 2014-09-18 | configure.ml: opam camlp5 + system ocaml works | Pierre Boutillier |
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau |
| 2014-09-17 | Change some Defined into Qed. | Guillaume Melquiond |
| 2014-09-17 | Add some missing Proof statements. | Guillaume Melquiond |
| 2014-09-17 | Remove pointless regex for '""' as the empty string already matches it. | Guillaume Melquiond |
| 2014-09-17 | Revert "coqc: execvp is now available even on win32" | Enrico Tassi |
| 2014-09-17 | win32: remove outdated splash screen | Enrico Tassi |
| 2014-09-17 | Fix highlighting of "Hint Unfold" and "Hint Rewrite". | Guillaume Melquiond |
| 2014-09-17 | Properly highlight the Export keyword. | Guillaume Melquiond |
| 2014-09-17 | Fix ambiguous regex in syntax highlighting. | Guillaume Melquiond |
| 2014-09-17 | Change an axiom into a definition. | Guillaume Melquiond |
| 2014-09-17 | Fix broken syntax highlighting for Coq files using "Proof constr". | Guillaume Melquiond |
| 2014-09-17 | win32: bring back the coq icon in the coqide binary | Enrico Tassi |
| 2014-09-17 | win32: use subsystem windows on windows (and not console) | Enrico Tassi |
| 2014-09-17 | Revert "While resolving typeclass evars in clenv, touch only the ones that ap... | Matthieu Sozeau |
| 2014-09-17 | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau |
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-16 | Undo prints only if coqtop || emacs | Enrico Tassi |
| 2014-09-16 | better error message | Enrico Tassi |
| 2014-09-16 | fix test-suite/success/decl_mode.v | Enrico Tassi |
| 2014-09-16 | More on printing references applied to implicit arguments. | Hugo Herbelin |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-15 | Adapting ltac output test to new interpretation of binders. | Hugo Herbelin |
| 2014-09-15 | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin |
| 2014-09-15 | Not printing goal name (reinstalled by mistake in a previous commit). | Hugo Herbelin |
| 2014-09-15 | Fixing line break in test for #3559. | Hugo Herbelin |
| 2014-09-15 | Fix timing of evar-normalisation of goals in [Ftactic.nf_enter]. | Arnaud Spiwack |
| 2014-09-15 | Ltac names in binders: some Ltac values can be seen both as terms and identif... | Arnaud Spiwack |
| 2014-09-15 | Fix: when interpreting a identifier in pretying, use the Ltac identifier subs... | Arnaud Spiwack |
| 2014-09-15 | Fix a bug in the naming of binders. | Arnaud Spiwack |
| 2014-09-15 | A small pass of code cleaning and clenv removing in Rewrite. | Pierre-Marie Pédrot |
| 2014-09-15 | Fixing bug #3619 in emacs mode. | Hugo Herbelin |
| 2014-09-15 | Avoid backtracking in typeclass search if a solution for a closed | Matthieu Sozeau |
| 2014-09-15 | Fix bug #3610, allowing betaiotadelta reduction while unifying types of | Matthieu Sozeau |
| 2014-09-15 | Fix bug #3621, using fold_left2 on arrays of the same size only. | Matthieu Sozeau |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-15 | Removing one Evd.merge in Rewrite. | Pierre-Marie Pédrot |
| 2014-09-15 | More invariants in Rewrite unification. | Pierre-Marie Pédrot |
| 2014-09-15 | The unifying functions of Rewrite uses the return types of strategies. | Pierre-Marie Pédrot |
