aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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 PR #867: Removing a redundant universe instance information in native c...Maxime Dénès
2017-07-10Removing a redundant universe instance information in native compute.Pierre-Marie Pédrot
2017-07-06Merge PR #853: Clean 'with Definition' implementation.Maxime Dénès
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-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
2017-06-30Add doc for inversion_sigma to RefMan-tacJason Gross
2017-06-30Update CHANGES with inversion_sigma entryJason Gross
2017-06-30Update .gitignore with doc/tutorial/Tutorial.v.outJason Gross
2017-06-30Fix more potential quoting issues: COQBIN , COQLIBJason Gross
2017-06-30Also quote $(COQLIB)/grammarJason Gross
2017-06-30Create a variable for CAMLDOC in CoqMakefile.inJason Gross
2017-06-30Quote $(OCAMLFIND) in CoqMakefile.in for WindowsJason Gross
2017-06-30Merge PR#846: Fix OS X Travis by pinning OCaml version.Maxime Dénès
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-30Fix OS X Travis by pinning OCaml version.Théo Zimmermann
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with...Maxime Dénès
2017-06-27Merge PR#731: Mini-cleaning around OCaml file namesMaxime Dénès
2017-06-27A cleaning phase about ocaml file names.Hugo Herbelin
2017-06-27Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied.Maxime Dénès
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26Merge PR#825: Ignore all PDF files.Maxime Dénès
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-26Bump version number to 8.6.1.Maxime Dénès
2017-06-26Fix libpcre dependency issue under Windows.Maxime Dénès
2017-06-26Fix proxy setting issueMichael Soegtrop
2017-06-26Fixes bug #5561,#5562 in Windows build systemMichael Soegtrop
2017-06-26Merge PR#756: Fix Bug #5574, document function scopeMaxime Dénès
2017-06-23Merge PR#824: Fix printersMaxime Dénès
2017-06-23Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremPr...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 20:57:36 +0000