aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* RefMan, ch. 1 and 2: avoiding using the name "constant" whenGravatar Hugo Herbelin2015-12-06
* RefMan, ch. 4: Consistent use of the terms local context and global environment.Gravatar Hugo Herbelin2015-12-06
* RefMan, ch. 4: Terminology constant/names.Gravatar Hugo Herbelin2015-12-06
* RefMan, ch. 4: Minor changes for spacing, clarity.Gravatar Hugo Herbelin2015-12-06
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* Fix CHANGES.Gravatar Hugo Herbelin2015-12-05
* Fix in setoid_rewrite in Type: avoid the generation of a rigid universeGravatar Matthieu Sozeau2015-12-04
* Univs: fix bug #4443.Gravatar Matthieu Sozeau2015-12-03
* Improving over printing of let-tuple (see #4447).Gravatar Hugo Herbelin2015-12-03
* Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
* Slight simplification of code for pat/constr.Gravatar Hugo Herbelin2015-12-02
* Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* Update history of revisions.Gravatar Hugo Herbelin2015-12-02
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
* Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
* Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
* Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
* vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
* Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
* Test-suite files for closed bugsGravatar Matthieu Sozeau2015-11-28
* Closed bugs.Gravatar Matthieu Sozeau2015-11-28
* Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Avoid recording spurious Set <= Top.i constraints which are alwaysGravatar Matthieu Sozeau2015-11-27
* Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
* Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
* Make the pretty printer resilient to incomplete nametab (progress on #4363).Gravatar Enrico Tassi2015-11-26
* Adding the Printing Projections options to the index.Gravatar Pierre-Marie Pédrot2015-11-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 10:33:53 +0000