| Commit message (Expand) | Author | Age |
|---|
| * | Fix constrMatching as well as change/e_contextually to allow |  Matthieu Sozeau | 2014-09-18 |
| * | Fix debug printing with primitive projections. | Matthieu Sozeau | 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-18 |
| * | 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-17 |
| * | 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-16 |
| * | 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 |
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Enrico Tassi
Pierre Boutillier
Guillaume Melquiond
Arnaud Spiwack