aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* Simplifying an instantiation function using subst_of_rel_context_instance.Gravatar Hugo Herbelin2015-12-05
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
* Experimenting documentation of the Vars.subst functions.Gravatar Hugo Herbelin2015-12-05
* Contracting one extra beta-redex on the fly when typing branches of "match".Gravatar Hugo Herbelin2015-12-05
* A few renaming and simplification in inductive.ml.Gravatar Hugo Herbelin2015-12-05
* Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* An example in centralizing similar functions to a common place so thatGravatar Hugo Herbelin2015-12-05
* Using x in output test-suite Cases.v (cosmetic).Gravatar Hugo Herbelin2015-12-05
* Ensuring that documentation of mli code works in the presence of utf-8Gravatar Hugo Herbelin2015-12-05
* Getting rid of some quoted tactics in Tauto.Gravatar Pierre-Marie Pédrot2015-12-05
* Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
* Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* Removing the last use of valueIn in Tauto.Gravatar Pierre-Marie Pédrot2015-12-04
* Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
* Removing the globTacticIn primitive.Gravatar Pierre-Marie Pédrot2015-12-03
* Fixing Tauto compilation for older versions of OCaml.Gravatar Pierre-Marie Pédrot2015-12-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
* | Removing the use of tacticIn in Tauto.Gravatar Pierre-Marie Pédrot2015-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
* | Removing dead code in Obligations.Gravatar Pierre-Marie Pédrot2015-12-02
* | New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
* | Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
| * vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
* | Simplify coqdep lexer by removing global references.Gravatar Guillaume Melquiond2015-11-30
| * Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * 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
* | More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 03:00:09 +0000