aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-12-10RefMan, ch. 4: Consistently using "constant" for names assumed or definedHugo Herbelin
2015-12-10RefMan, ch. 4: Fixing the definition of terms considered in the section.Hugo Herbelin
2015-12-09Print Assumptions: improve detection of case on an axiom of FalseEnrico Tassi
2015-12-09Remove remaining occurrences of Unix.readdir.Guillaume Melquiond
2015-12-09Replace Unix.readdir by Sys.readdir in dir cache.Emilio Jesus Gallego Arias
2015-12-09a few edits to the universe polymorphism section of the manualGregory Malecha
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-12-09The unshelve tactical now takes future goals into account.Pierre-Marie Pédrot
2015-12-09Fixing parsing of the unshelve tactical.Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma...Matej Kosik
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-06RefMan, ch. 1 and 2: avoiding using the name "constant" whenHugo Herbelin
2015-12-06RefMan, ch. 4: Consistent use of the terms local context and global environment.Hugo Herbelin
2015-12-06RefMan, ch. 4: Terminology constant/names.Hugo Herbelin
2015-12-06RefMan, ch. 4: Minor changes for spacing, clarity.Hugo Herbelin
2015-12-05Fixing compilation with old CAMLPX versions.Pierre-Marie Pédrot
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-12-05Leveraging GADTs to provide a better Dyn API.Pierre-Marie Pédrot
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-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-05Fix CHANGES.Hugo 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-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
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-03Univs: fix bug #4443.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 09:35:47 +0000