aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
Delaying also some computation needed for printing to the time of really printing it.
2017-07-06Merge PR #853: Clean 'with Definition' implementation.Maxime Dénès
2017-07-05Fix typo in documentation for identityTej Chajed
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
2017-07-05use Int.equal instead of polymorphic =Paul Steckler
2017-07-05[travis] Remove CompCert version check hack.Emilio Jesus Gallego Arias
We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy .
2017-07-05Extraction TestCompile foo : a new command for extraction + ocamlcPierre Letouzey
Extraction TestCompile foo is equivalent to: Extraction "/tmp/testextraction1234.ml" foo ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml This command isn't meant for the end user, but rather as an helper for test-suite scripts. It only works with extraction to OCaml, and the generated code should be standalone.
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-05Makefile: fails if some .vo or .cm* file has no sourcePierre Letouzey
This should help preventing weird compilation failures due to leftover object files after deleting or moving some source files By the way: - use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason for the suggestion) - rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more than version control stuff nowadays
2017-07-04Revert fiat-crypto overlayJason Gross
Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
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
This code was a sketch of what to do when we properly implement module-level handling of instanciation of definitions by inductive types. It was completely dead code, called after an error, and somewhat incorrect. Instead of letting it bitrot, we remove it.
2017-07-03Removing a few suspicious functions from the kernel.Pierre-Marie Pédrot
These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead.
2017-07-03Do not add original constraints to the environment in 'with Definition' check.Pierre-Marie Pédrot
This was useless, because immediate constraints are assumed to already be in the current environment, while deferred constraints are useless for the conversion check of the definition types, as they only appear in the opaque body. This also clarifies a bit what is going on in the typing of module constraints w.r.t. global universes.
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
We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it.
2017-06-30Remove doc/refman/RefMan-ind.texJason Gross
It does not seem to be referred to by any file, and does not seem to be built by any implicit rules.
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
In case COQLIB has backslashes, as it does on Windows, or spaces
2017-06-30Create a variable for CAMLDOC in CoqMakefile.inJason Gross
2017-06-30Quote $(OCAMLFIND) in CoqMakefile.in for WindowsJason Gross
This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
2017-06-30Better support for make TIMED=1 on WindowsJason Gross
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
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-30Mention again how to report bug and get version number.Théo Zimmermann
As suggested by @psteckler.
2017-06-30Fix OS X Travis by pinning OCaml version.Théo Zimmermann
2017-06-29Fix Zmod_div.Russell O'Connor
2017-06-29Use forall for consistencyroconnor-blockstream
2017-06-29Add Z.mod_div lemma to standard library.Russell O'Connor
2017-06-29Better phrasing.Théo Zimmermann
2017-06-29More substance on discouraged practices.Théo Zimmermann
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-29Some more corrections to the tutorial.Théo Zimmermann
2017-06-29Mask the reliance on coqtop.Théo Zimmermann
2017-06-29[meta] [api] Fix META file for API introduction.Emilio Jesus Gallego Arias
2017-06-28Update the Tutorial.Théo Zimmermann
2017-06-28A fix for #5598 (no discharge of Existing Classes referring to local variables).Hugo Herbelin
2017-06-28Avoiding an optional int rather than using -1 to encode a local flag.Hugo Herbelin
Also giving the proper local flag to the hint registration, even on a Global instance, since the instance discharge manage itself the redefinition of a hint.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 07:04:27 +0000