| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-11 | Cleaning up the implementation of module subtyping in the kernel. | Pierre-Marie Pédrot | |
| We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants. | |||
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-11 | Less footguns in universe handling: remove subst_instance_context. | Pierre-Marie Pédrot | |
| This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone. | |||
| 2017-07-11 | Asserting that monomorphic section variables have no abstracted context. | Pierre-Marie Pédrot | |
| 2017-07-11 | Getting rid of simple calls to AUContext.instance. | Pierre-Marie Pédrot | |
| This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. | |||
| 2017-07-11 | Merge PR #867: Removing a redundant universe instance information in native ↵ | Maxime Dénès | |
| compute. | |||
| 2017-07-10 | Removing a redundant universe instance information in native compute. | Pierre-Marie Pédrot | |
| Global declarations used to carry universe instances with them, but it turns out this information is not used anywhere. Instead, instances were already properly encoded as the first argument of polymorphic definitions. | |||
| 2017-07-06 | Merge PR #853: Clean 'with Definition' implementation. | Maxime Dénès | |
| 2017-07-05 | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès | |
| 2017-07-05 | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn | Maxime Dénès | |
| 2017-07-05 | Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows | Maxime Dénès | |
| 2017-07-05 | Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.out | Maxime Dénès | |
| 2017-07-05 | Merge PR #832: Document an example `Makefile` for `coq_makefile` | Maxime Dénès | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-07-04 | Removing 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-03 | Removing 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-03 | Do 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-01 | Update RefMan-syn.tex | william-lawvere | |
| 2017-07-01 | Merge remote-tracking branch 'upstream/trunk' into trunk | William Lawvere | |
| 2017-07-01 | RefMan-gal: improve grammar | William Lawvere | |
| 2017-07-01 | RefMan-syn: grammar edit | William Lawvere | |
| 2017-06-30 | Document 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-30 | Add doc for inversion_sigma to RefMan-tac | Jason Gross | |
| 2017-06-30 | Update CHANGES with inversion_sigma entry | Jason Gross | |
| 2017-06-30 | Update .gitignore with doc/tutorial/Tutorial.v.out | Jason Gross | |
| 2017-06-30 | Fix more potential quoting issues: COQBIN , COQLIB | Jason Gross | |
| 2017-06-30 | Also quote $(COQLIB)/grammar | Jason Gross | |
| In case COQLIB has backslashes, as it does on Windows, or spaces | |||
| 2017-06-30 | Create a variable for CAMLDOC in CoqMakefile.in | Jason Gross | |
| 2017-06-30 | Quote $(OCAMLFIND) in CoqMakefile.in for Windows | Jason Gross | |
| This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620) | |||
| 2017-06-30 | Merge PR#846: Fix OS X Travis by pinning OCaml version. | Maxime Dénès | |
| 2017-06-30 | Merge PR#843: closing bug #5618 introduce by PR 828 | Maxime Dénès | |
| 2017-06-30 | Fix OS X Travis by pinning OCaml version. | Théo Zimmermann | |
| 2017-06-29 | closing bug #5618 introduce by PR 828 | Julien Forest | |
| 2017-06-27 | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵ | Maxime Dénès | |
| with make -j4 | |||
| 2017-06-27 | Merge PR#731: Mini-cleaning around OCaml file names | Maxime Dénès | |
| This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions. | |||
| 2017-06-27 | A cleaning phase about ocaml file names. | Hugo Herbelin | |
| Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names. | |||
| 2017-06-27 | Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied. | Maxime Dénès | |
| 2017-06-26 | Merge PR#826: Put plugin exports in the right compatibility file | Maxime Dénès | |
| 2017-06-26 | Merge PR#825: Ignore all PDF files. | Maxime Dénès | |
| 2017-06-26 | Merge PR#828: closing bug #4250 | Maxime Dénès | |
| 2017-06-26 | Bump version number to 8.6.1. | Maxime Dénès | |
| 2017-06-26 | Fix libpcre dependency issue under Windows. | Maxime Dénès | |
| 2017-06-26 | Fix proxy setting issue | Michael Soegtrop | |
| 2017-06-26 | Fixes bug #5561,#5562 in Windows build system | Michael Soegtrop | |
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès | |
| 2017-06-23 | Merge PR#824: Fix printers | Maxime Dénès | |
| 2017-06-23 | Merge PR#821: [vernac] Remove stale bool parameter from ↵ | Maxime Dénès | |
| `VernacStartTheoremProof` | |||
| 2017-06-23 | Merge PR#820: [ide] Correct more merging errors. | Maxime Dénès | |
| 2017-06-23 | Merge PR#815: STM: par: report no error to UIs in non-solve mode | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |