aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix for case-insensitive path looking continued (#2554): Adding aGravatar Hugo Herbelin2015-11-25
* Generalizing the patch to bug #2554 on fixing path looking withGravatar Hugo Herbelin2015-11-25
* Heuristic to check the version of lablgtk2 in configure.ml.Gravatar Pierre-Marie Pédrot2015-11-25
* Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Gravatar Hugo Herbelin2015-11-25
* Advertising that CoqIDE requires lablgtk >= 2.16Gravatar Pierre-Marie Pédrot2015-11-25
* Checking lablgtk version in configure. Fix bug #4423.Gravatar Pierre-Marie Pédrot2015-11-25
* Univs: carry on universe substitution when defining obligations ofGravatar Matthieu Sozeau2015-11-24
* Fixing an old typo in Retyping, found by Matej.Gravatar Hugo Herbelin2015-11-24
* Fix generation of equality schemes on polymorphic equality types.Gravatar Matthieu Sozeau2015-11-23
* Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
* Fixing a vm_compute bug in the presence of let-ins among theGravatar Hugo Herbelin2015-11-22
* Fixing a bug of adjust_subst_to_rel_context.Gravatar Hugo Herbelin2015-11-22
* Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* Univs: generation of induction schemes should not generated uselessGravatar Matthieu Sozeau2015-11-20
* Univs: fix type_of_global_in_context not returning instantiated universe cont...Gravatar Matthieu Sozeau2015-11-20
* Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Gravatar Pierre-Marie Pédrot2015-11-19
* Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Fixing fix c71aa6b to primitive projections.Gravatar Hugo Herbelin2015-11-18
* Fix a bug preventing the generation of graphs when doing multipleGravatar Matthieu Sozeau2015-11-18
* Improve error message.Gravatar Maxime Dénès2015-11-18
* MacOS package script: do not fail if link to /Applications already exists.Gravatar Maxime Dénès2015-11-18
* Slightly documenting code for building primitive projections.Gravatar Hugo Herbelin2015-11-18
* Fixing logical bugs in the presence of let-ins in computiong primitiveGravatar Hugo Herbelin2015-11-18
* More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Being more precise and faithful about the origin of the file reportingGravatar Hugo Herbelin2015-11-16
* Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Gravatar Matthieu Sozeau2015-11-13
* MacOS package script: do not fail if directory _dmg already exists.Gravatar Maxime Dénès2015-11-13
* Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
* Fixed test-suite file for bug #3998.Gravatar Matthieu Sozeau2015-11-12
* Update CHANGESGravatar Jason Gross2015-11-12
* Script building MacOS package.Gravatar Maxime Dénès2015-11-12
* Now closed.Gravatar Matthieu Sozeau2015-11-11
* Ensure that conversion is called on terms of the same type inGravatar Matthieu Sozeau2015-11-11
* Fix bug #3998: when using typeclass resolution for conversion, allowGravatar Matthieu Sozeau2015-11-11
* Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
* Typo.Gravatar Hugo Herbelin2015-11-10
* Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
* Test for bug #4404.Gravatar Pierre-Marie Pédrot2015-11-10
* Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Gravatar Pierre-Marie Pédrot2015-11-10
* Pushing the backtrace in conversion anomalies.Gravatar Pierre-Marie Pédrot2015-11-09
* Fixing output test Existentials.v after eec77191b.Gravatar Hugo Herbelin2015-11-07
* Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Gravatar Hugo Herbelin2015-11-07
* Tests for syntax "Show id" and [id]:tac (shelved or not).Gravatar Hugo Herbelin2015-11-07
* Fixing documention of Add Printing Coercion.Gravatar Hugo Herbelin2015-11-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:03:57 +0000