| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik | |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik | |
| 2015-12-15 | API: documenting context_chop and removing a duplicate. | Hugo Herbelin | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-05 | Fixing compilation of mli documentation. | Hugo Herbelin | |
| Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed. | |||
| 2015-12-05 | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin | |
| It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. | |||
| 2015-12-05 | About building of substitutions from instances. | Hugo Herbelin | |
| Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. | |||
| 2015-12-05 | Moving three related small half-general half-ad-hoc utility functions | Hugo Herbelin | |
| next to each other, waiting for possible integration into a more uniform API. | |||
| 2015-12-01 | Remove unneeded fixpoint in normalize_context_set. Note that it is no | Matthieu Sozeau | |
| longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l). | |||
| 2015-11-26 | More efficient implementation of equality-up-to-universes in Universes. | Pierre-Marie Pédrot | |
| Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice. | |||
| 2015-11-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-26 | More invariants in UState. | Pierre-Marie Pédrot | |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot | |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Removing some unsafe uses of monotonicity. | Pierre-Marie Pédrot | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-18 | Adding a notion of monotonous evarmap. | Pierre-Marie Pédrot | |
| 2015-10-17 | Clarifying and documenting the UState API. | 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-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-27 | Removing meta_with_name from Evd. | Pierre-Marie Pédrot | |
| 2015-09-27 | Removing subst_defined_metas_evars from Evd. | Pierre-Marie Pédrot | |
| 2015-09-27 | Removing uselessly duplicated function in Evd. | Pierre-Marie Pédrot | |
| 2015-09-26 | Hardening the API of evarmaps. | Pierre-Marie Pédrot | |
| The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap. | |||
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-27 | Fix documentation. | Matthieu Sozeau | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-07 | Adding a primitive to the tactic monad to modify the exceptional content. | Pierre-Marie Pédrot | |
| 2015-05-06 | Exposing the minimal amount of internal of the Logic monad in order to | Pierre-Marie Pédrot | |
| allow reusability of the implementation throughout the Coq codebase. We effectively feature a generalized version of the logical monad where the input state, the output state and the inner exception can be arbitrarily chosen. This will allow for more efficient implementations of close variants of the monad. | |||
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-28 | Moving Proofview_monad to the engine/ folder. | Pierre-Marie Pédrot | |
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | |
| together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |