| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | |
| goal is under focus and which support returning a relevant output. | |||
| 2016-09-05 | Fast path in push_rel_context_to_named_context. | Pierre-Marie Pédrot | |
| Essentially, we do not reconstruct the named_context_val when the rel_context is empty. | |||
| 2016-09-02 | Fast path in whd_evar. | Pierre-Marie Pédrot | |
| Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined. | |||
| 2016-09-01 | Short documentation, filling TODO's in evd.mli. | Hugo Herbelin | |
| 2016-08-25 | Do not export an internal function in Namegen. | Pierre-Marie Pédrot | |
| 2016-08-17 | Two protections against failures when printing evar_map. | Hugo Herbelin | |
| Delimit the scope of the failure to ease potential need for debugging the debugging printer. Protect against one of the causes of failure (calling get_family_sort_of with non-synchronized sigma). | |||
| 2016-08-17 | Fixing printing in debugger (no global env in debugger). | Hugo Herbelin | |
| 2016-08-16 | Efficiently generate the pretyping contexts. | Pierre-Marie Pédrot | |
| We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better. | |||
| 2016-08-10 | Remove unused optional "predicative" argument. | Guillaume Melquiond | |
| 2016-08-06 | Using a dedicated kind of substitutions in evar name generation. | Pierre-Marie Pédrot | |
| This saves a quadratic allocation by replacing arrays with maps. | |||
| 2016-08-05 | Using the extended contexts in pretyping. | Pierre-Marie Pédrot | |
| In addition to sharing, we also delay the computation of the environment in a by-need fashion. | |||
| 2016-08-04 | Use sets instead of lists for names to avoid in evar generation. | Pierre-Marie Pédrot | |
| 2016-08-04 | Simplifying code in evar generation. | Pierre-Marie Pédrot | |
| We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences. | |||
| 2016-08-04 | Exporting the renaming API for evar declaration. | Pierre-Marie Pédrot | |
| 2016-07-08 | Fixing #4906 (regression in printing an error message). | Hugo Herbelin | |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵ | Pierre Letouzey | |
| module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a | |||
| 2016-06-29 | Univ: Use loc even if there are more unbound levels | Matthieu Sozeau | |
| 2016-06-29 | Univs: add source locations of levels | Matthieu Sozeau | |
| For better error messages. The API change is backwards compatible, using a new optional argument. | |||
| 2016-06-24 | Optmimize the subst tactic. | Pierre-Marie Pédrot | |
| Take advantage that the provided term is always a variable in Equality.is_eq_x. | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not allocate a closure in the main loop, and do so only when needed. | |||
| 2016-06-24 | Optimize the clear tactic. | Pierre-Marie Pédrot | |
| We do not check for presence of a variable in a global definition when we know that this variable was not present in the section. | |||
| 2016-06-23 | Better algorithm for variable deambiguation in term printing. | Pierre-Marie Pédrot | |
| We do not recompute shortest name identifier for global references that were already traversed. Furthermore, we share the computation of identifiers between invokations of the name generating function. This drastically speeds up detyping for huge goals, further mitigating the shortcomings of the fix for bug #4777. | |||
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-06-16 | Proofview: extensions for backtracking eauto | Matthieu Sozeau | |
| unshelve_goals is used to correctly register dependent subgoals that have to be solved. Resolution may fail to do so using hints, so we have to put them back as goals in that case. The shelf is a good interface for doing that. unifiable can be used outside proofview to detect dependencies between goals. This might be better in another module. | |||
| 2016-06-16 | Implement limited proof search and iterative deepening. | Matthieu Sozeau | |
| Fix typo in proofview | |||
| 2016-06-16 | Merge 'pr/191' into trunk | Enrico Tassi | |
| 2016-06-14 | Merge remote-tracking branch 'origin/pr/173' into trunk | Enrico Tassi | |
| This is the "error resiliency" mode for STM | |||
| 2016-06-14 | Fix a typo in proofs/proofview.mli. | Cyprien Mangin | |
| 2016-06-14 | Fix usage of Pervasives in goal selectors. | Cyprien Mangin | |
| 2016-06-14 | Add a comment about the use of a zipper, for clarity. | Cyprien Mangin | |
| 2016-06-14 | Add a [CList.partitioni] function. | Cyprien Mangin | |
| 2016-06-14 | Add goal range selectors. | Cyprien Mangin | |
| You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5. | |||
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | |
| 2016-06-06 | STM: proof block detection for bullets and { block } | Enrico Tassi | |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias | |
| This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work. | |||
| 2016-05-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-05-04 | Normalizing the names of dynamic types to follow a typ_* scheme. | Pierre-Marie Pédrot | |
| 2016-05-04 | Interpretation function can return any untyped value. | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing external uses of Val.inject and making Geninterp.interp return Val.t | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Getting rid of the Geninterp.generic_interp function. | Pierre-Marie Pédrot | |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving Ftactic and Geninterp to the engine folder. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent of Logic. | Pierre-Marie Pédrot | |
| 2016-02-19 | Allowing to attach location to universes in UState. | Pierre-Marie Pédrot | |
| 2016-02-15 | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | |
| 2016-02-15 | Monotonizing the Evarutil module. | Pierre-Marie Pédrot | |
| Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now. | |||
| 2016-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |