aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-17Merge PR #865: RefMan-ext: fix some typosMaxime Dénès
2017-07-17Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat...Maxime Dénès
2017-07-14Update with non structurally recursivewilliam-lawvere
2017-07-13Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelMaxime Dénès
2017-07-12Adding a comment regarding De Bruijn universe indices in the kernel.Pierre-Marie Pédrot
2017-07-11Merge PR #871: Update Travis badge following the switch to masterMaxime Dénès
2017-07-11Update Travis badge following the switch to masterThéo Zimmermann
2017-07-11Moving the last bits of abtraction-breaking code out of the kernel.Pierre-Marie Pédrot
2017-07-11Fix nonsensical universe abstraction in the kernel.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the checker.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Asserting that monomorphic section variables have no abstracted context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-11Merge branch 'v8.7'Maxime Dénès
2017-07-11Merge PR #858: [travis] Remove CompCert version check hack.Maxime Dénès
2017-07-11Merge PR #867: Removing a redundant universe instance information in native c...Maxime Dénès
2017-07-11Merge PR #860: use Int.equal instead of polymorphic =Maxime Dénès
2017-07-10Removing a redundant universe instance information in native compute.Pierre-Marie Pédrot
2017-07-08Adding support for bindings tags to explicit prefix/suffix rather than colors.Hugo Herbelin
2017-07-07RefMan-ext: fix some typosWilliam Lawvere
2017-07-07Merge PR #863: Fixing environment in warning "Projection value has no head co...Maxime Dénès
2017-07-07Merge PR #842: Update the Tutorial.Maxime Dénès
2017-07-07Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...Maxime Dénès
2017-07-07Merge PR #835: Remove doc/refman/RefMan-ind.texMaxime Dénès
2017-07-07Set version to 8.7.0~alpha.Maxime Dénès
2017-07-07Merge PR #844: Better support for make TIMED=1 on WindowsMaxime Dénès
2017-07-07Merge PR #800: Enable fiat-cryptoMaxime Dénès
2017-07-07Fixing environment in warning "Projection value has no head constant".Hugo Herbelin
2017-07-06Merge PR #853: Clean 'with Definition' implementation.Maxime Dénès
2017-07-05use Int.equal instead of polymorphic =Paul Steckler
2017-07-05[travis] Remove CompCert version check hack.Emilio Jesus Gallego Arias
2017-07-05Merge PR #837: Add inversion_sigma to CHANGES and to docMaxime Dénès
2017-07-05Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synMaxime Dénès
2017-07-05Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for WindowsMaxime Dénès
2017-07-05Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.outMaxime Dénès
2017-07-05Merge PR #832: Document an example `Makefile` for `coq_makefile`Maxime Dénès
2017-07-04Revert fiat-crypto overlayJason Gross
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-07-04Removing dead code in Subtyping.Pierre-Marie Pédrot
2017-07-03Removing a few suspicious functions from the kernel.Pierre-Marie Pédrot
2017-07-03Do not add original constraints to the environment in 'with Definition' check.Pierre-Marie Pédrot
2017-07-01Update RefMan-syn.texwilliam-lawvere
2017-07-01Merge remote-tracking branch 'upstream/trunk' into trunkWilliam Lawvere
2017-07-01RefMan-gal: improve grammarWilliam Lawvere
2017-07-01RefMan-syn: grammar editWilliam Lawvere
2017-06-30Document an example `Makefile` for `coq_makefile`Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 20:49:05 +0000