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