aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-12-05Making output of target source-doc a bit less verbose.Hugo Herbelin
2015-12-05Fixing compilation of mli documentation.Hugo Herbelin
2015-12-05Fix to previous commit (ClassicalFacts.v).Hugo Herbelin
2015-12-05Adding proofs on the relation between excluded-middle and minimization.Hugo Herbelin
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Slight simplification of the code of primitive projection (in relationHugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05Simplifying an instantiation function using subst_of_rel_context_instance.Hugo Herbelin
2015-12-05About building of substitutions from instances.Hugo Herbelin
2015-12-05Experimenting documentation of the Vars.subst functions.Hugo Herbelin
2015-12-05Contracting one extra beta-redex on the fly when typing branches of "match".Hugo Herbelin
2015-12-05A few renaming and simplification in inductive.ml.Hugo Herbelin
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-05An example in centralizing similar functions to a common place so thatHugo Herbelin
2015-12-05Using x in output test-suite Cases.v (cosmetic).Hugo Herbelin
2015-12-05Ensuring that documentation of mli code works in the presence of utf-8Hugo Herbelin
2015-12-05Getting rid of some quoted tactics in Tauto.Pierre-Marie Pédrot
2015-12-04Specializing the Dyn module to each usecase.Pierre-Marie Pédrot
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-04Removing the last use of valueIn in Tauto.Pierre-Marie Pédrot
2015-12-04Removing dynamic inclusion of constrs in tactic AST.Pierre-Marie Pédrot
2015-12-04Getting rid of dynamic hacks in Setoid_newring.Pierre-Marie Pédrot
2015-12-03Removing the globTacticIn primitive.Pierre-Marie Pédrot
2015-12-03Fixing Tauto compilation for older versions of OCaml.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-12-03Removing the use of tacticIn in Tauto.Pierre-Marie Pédrot
2015-12-02Adding a target report to test-suite's Makefile to get a short summary.Hugo Herbelin
2015-12-02Slight simplification of code for pat/constr.Hugo Herbelin
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
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-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-12-01New algorithm for universe cycle detections.Jacques-Henri Jourdan
2015-12-01Remove unneeded fixpoint in normalize_context_set. Note that it is noMatthieu Sozeau
2015-12-01vio: fix argument parsing (progress on #4442)Enrico Tassi
2015-11-30Simplify coqdep lexer by removing global references.Guillaume Melquiond
2015-11-30Test for bug #4149.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 05:52:28 +0000