| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-21 | Finer-grained types for toplevel values. | Pierre-Marie Pédrot | |
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot | |
| 2015-12-18 | Tying the loop in tactic printing API. | Pierre-Marie Pédrot | |
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-07 | Fixing a minor problem in Makefile.build that was prevening ↵ | Matej Kosik | |
| "dev/printers.cma" to be loadable within "ocamldebug". | |||
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-05 | Factorizing unsafe code by relying on the new Dyn module. | Pierre-Marie Pédrot | |
| 2015-12-05 | Ensuring that documentation of mli code works in the presence of utf-8 | Hugo Herbelin | |
| characters. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Update history of revisions. | Hugo Herbelin | |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-18 | MacOS package script: do not fail if link to /Applications already exists. | Maxime Dénès | |
| 2015-11-16 | Being more precise and faithful about the origin of the file reporting | Hugo Herbelin | |
| about the prehistory of Coq. | |||
| 2015-11-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-13 | MacOS package script: do not fail if directory _dmg already exists. | Maxime Dénès | |
| 2015-11-12 | Script building MacOS package. | Maxime Dénès | |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | |
| presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | |||
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-28 | Refine Gregory Malecha's patch on VM and universe polymorphism. | Maxime Dénès | |
| - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. | |||
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe ↵ | Gregory Malecha | |
| polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. | |||
| 2015-10-27 | Type-safe Egramml.grammar_prod_item. | Pierre-Marie Pédrot | |
| 2015-10-26 | Pcoq entries are given a proper module. | Pierre-Marie Pédrot | |
| Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant. | |||
| 2015-10-18 | Adding a notion of monotonous evarmap. | Pierre-Marie Pédrot | |
| 2015-10-17 | Dedicated file for universe unification context manipulation. | Pierre-Marie Pédrot | |
| This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar. | |||
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-14 | Reverting modifications in dev/top_printers pushed mistakenly. | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing perfomance issue of auto hints induced by universes. | Pierre-Marie Pédrot | |
| Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. | |||
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Minor typo in universe polymorphism doc. | Maxime Dénès | |
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | |
| 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. | |||
| 2015-10-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Updating versions history with data from Gérard. | Hugo Herbelin | |
| Adding Gérard's history file about V1-V5 versions. | |||
| 2015-10-02 | Update the history of versions with recent versions. | Hugo Herbelin | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau | |
| 2015-09-20 | Better debug printers for module paths. | Maxime Dénès | |
| Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now. | |||
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-17 | Fix Windows installer. | Guillaume Melquiond | |
| The theories/ directory contains no cmi/cmxs files when native_compute is disabled, so do not try to ship them. | |||
| 2015-08-22 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-08-17 | windows build scripts made more accurate in detecting failures | Enrico Tassi | |
| 2015-08-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-30 | A printer for printing constants of the env (maybe useful when there are not ↵ | Hugo Herbelin | |
| too many of them). | |||
| 2015-07-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-23 | adding a missing case for printing zippers. | Gregory Malecha | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-06-29 | Assumptions: more informative print for False axiom (Close: #4054) | Enrico Tassi | |
| When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0 | |||
| 2015-06-29 | win: compile with -debug | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |