aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-12-02Update history of revisions.Hugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-12-02Univs/Program: update the universe context with global universeMatthieu Sozeau
2015-12-02Fix bug #4444: Next Obligation performed after a Section opening wasMatthieu Sozeau
2015-12-02Add an option to deactivate compatibility printing of primitiveMatthieu Sozeau
2015-12-02Fix a bug in externalisation which prevented printing of projectionsMatthieu Sozeau
2015-12-01vio: fix argument parsing (progress on #4442)Enrico Tassi
2015-11-30Test for bug #4149.Pierre-Marie Pédrot
2015-11-28Test-suite files for closed bugsMatthieu Sozeau
2015-11-28Closed bugs.Matthieu Sozeau
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-27Avoid recording spurious Set <= Top.i constraints which are alwaysMatthieu Sozeau
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
2015-11-26Fixing the "parsing rules with idents later declared as keywords" problem.Hugo Herbelin
2015-11-26Make the pretty printer resilient to incomplete nametab (progress on #4363).Enrico Tassi
2015-11-26Adding the Printing Projections options to the index.Pierre-Marie Pédrot
2015-11-25Fix for case-insensitive path looking continued (#2554): Adding aHugo Herbelin
2015-11-25Generalizing the patch to bug #2554 on fixing path looking withHugo Herbelin
2015-11-25Heuristic to check the version of lablgtk2 in configure.ml.Pierre-Marie Pédrot
2015-11-25Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Hugo Herbelin
2015-11-25Advertising that CoqIDE requires lablgtk >= 2.16Pierre-Marie Pédrot
2015-11-25Checking lablgtk version in configure. Fix bug #4423.Pierre-Marie Pédrot
2015-11-24Univs: carry on universe substitution when defining obligations ofMatthieu Sozeau
2015-11-24Fixing an old typo in Retyping, found by Matej.Hugo Herbelin
2015-11-23Fix generation of equality schemes on polymorphic equality types.Matthieu Sozeau
2015-11-23Fix output of universe arcs. (Fix bug #4422)Guillaume Melquiond
2015-11-22Fixing a vm_compute bug in the presence of let-ins among theHugo Herbelin
2015-11-22Fixing a bug of adjust_subst_to_rel_context.Hugo Herbelin
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-20Univs: generation of induction schemes should not generated uselessMatthieu Sozeau
2015-11-20Univs: fix type_of_global_in_context not returning instantiated universe cont...Matthieu Sozeau
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
2015-11-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Fixing fix c71aa6b to primitive projections.Hugo Herbelin
2015-11-18Fix a bug preventing the generation of graphs when doing multipleMatthieu Sozeau
2015-11-18Improve error message.Maxime Dénès
2015-11-18MacOS package script: do not fail if link to /Applications already exists.Maxime Dénès
2015-11-18Slightly documenting code for building primitive projections.Hugo Herbelin
2015-11-18Fixing logical bugs in the presence of let-ins in computiong primitiveHugo Herbelin
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-16Being more precise and faithful about the origin of the file reportingHugo Herbelin
2015-11-13Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Matthieu Sozeau
2015-11-13MacOS package script: do not fail if directory _dmg already exists.Maxime Dénès
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-12Fixed test-suite file for bug #3998.Matthieu Sozeau
2015-11-12Update CHANGESJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:49:49 +0000