| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2013-11-30 | Better heuristic for name generation backward compatibility. We fallback | Pierre-Marie Pédrot | |
| to old behaviour whenever we were in Program mode. | |||
| 2013-11-30 | Useless instantiation function exported in Evd. | Pierre-Marie Pédrot | |
| 2013-11-30 | Tentative fix to recover fresh name generation as it was before | Pierre-Marie Pédrot | |
| new-tacticals merge. This is essentially a revert of 6fea2f which broke the sacrosanct backward compatibility of name generation, thus breaking quite a lot of contribs. | |||
| 2013-11-29 | First stab at documenting Canonical Structures | Enrico Tassi | |
| 2013-11-29 | Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not | Hugo Herbelin | |
| supporting metas/evars). Fix of #3169 is by calling pretyping retyper rather than the non evar-aware kernel type-checker (since argument of vm_compute is supposed to be already typable). Support of metas/evars in vm is still to be done... | |||
| 2013-11-29 | Testsuite: flatten the 'bugs/opened' directory. | xclerc | |
| 2013-11-28 | Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused) | xclerc | |
| 2013-11-27 | Getting rid of goal-dependency in declarative mode argument evaluation. | Pierre-Marie Pédrot | |
| 2013-11-27 | Fixing abstract tactic by using a dummy name out of a declared proof. | Pierre-Marie Pédrot | |
| 2013-11-27 | Actually adding the grammar entry to handle tactics in terms. | Pierre-Marie Pédrot | |
| 2013-11-27 | Adding the necessary hooks to handle tactics in terms. | Pierre-Marie Pédrot | |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | |
| parsing is plugged. | |||
| 2013-11-27 | Old message Interp returns the state id so that one can BackTo it | Enrico Tassi | |
| 2013-11-27 | New option --help-XML-protocol to document the XML procol used by -ideslave | Enrico Tassi | |
| Serialize.ml spits out its own documentation. Not everything is statically checked, so it risks to get outdated. Ideas on how to statically/dynamically check that the doc is in sync are welcome. | |||
| 2013-11-27 | First stab at retrocompatible INTERP message | Enrico Tassi | |
| 2013-11-27 | Use my real email address in .mailmap | Enrico Tassi | |
| 2013-11-27 | Reduction: every n iterations a slaves process checks for interruption | Enrico Tassi | |
| I chose n to be 10000 iterations. It might be big, but a slave, to check for a termination request, has to pass the ball to the thread that sends "regularly" Ticks to the master process. Thread.yield is a system call, so we have to do it very rarely. | |||
| 2013-11-27 | STM: restart slave after every proof | Enrico Tassi | |
| The code now passes a cleanup function that, if slave is not killed, could be used to do some cleanup between two jobs. ATM I don't know how to reuse the worker without having it grow in space indefinitely. Running Gc.compact is too expensive. | |||
| 2013-11-27 | CoqIDE: show error message for parsing errors | Enrico Tassi | |
| 2013-11-26 | Adding a generic Int.Map using persistent arrays. | Pierre-Marie Pédrot | |
| 2013-11-26 | Do not use ugly Dyn features in the Quote plugin. Use instead the | Pierre-Marie Pédrot | |
| provided tactic environment to handle open terms. | |||
| 2013-11-25 | Remove the Hiddentac module. | Arnaud Spiwack | |
| Since the new proof engine, Hiddentac has been essentially trivial. Here is what happened to the functions defined there - Aliases, or tactics that were trivial to inline were systematically inlined - Tactics used only in tacinterp have been moved to tacinterp - Other tactics have been moved to a new module Tactics.Simple. | |||
| 2013-11-25 | Factoring: is_section_variable. | Arnaud Spiwack | |
| In 0c7a77, I inadvertantly re-defined an is_section_variable function. | |||
| 2013-11-25 | Tacinterp: fewer use of old-style goals. | Arnaud Spiwack | |
| There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics. I've changed some of them to explicitely take an environment and an evar_map instead. | |||
| 2013-11-25 | Typo resulting in bad eta-expansion of destructing let's body. | Hugo Herbelin | |
| Revealed by message on coq-club on 24/11/2013. | |||
| 2013-11-24 | Better implementation of summary unfreezing. | Pierre-Marie Pédrot | |
| 2013-11-24 | Adding fold_left / fold_right function to maps. | Pierre-Marie Pédrot | |
| 2013-11-24 | Updating new ftp link to old archives. | Hugo Herbelin | |
| 2013-11-24 | Hardening the reading function of vo files. | Pierre-Marie Pédrot | |
| 2013-11-24 | Slightly more efficient zip function in Closure. | Pierre-Marie Pédrot | |
| 2013-11-24 | Tweaking arity & allocation of some basic functions. | Pierre-Marie Pédrot | |
| 2013-11-23 | Small allocation improvement in Closure. | Pierre-Marie Pédrot | |
| 2013-11-23 | configure: typo in my last commit | Pierre Letouzey | |
| 2013-11-23 | Fixing bug #3165. | Pierre-Marie Pédrot | |
| 2013-11-22 | Remove some occurrences of obsolete operators | Stephane Glondu | |
| 2013-11-22 | configure: improve last fix | Pierre Letouzey | |
| Let's avoid the "if a=$(cmd ...)" since: - unless being a shell expert, it's not obvious it's testing the exit code of cmd. - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the exit code of cmd. Instead, we test the emptiness of the variable content afterwards | |||
| 2013-11-22 | Using hashes in Summary, like the previous commit did with Dyn. | Pierre-Marie Pédrot | |
| 2013-11-22 | Using hashes instead of strings in dynamic tags. In case of collision, an | Pierre-Marie Pédrot | |
| anomaly is raised. As there are very few tags defined in Coq code, this is very unlikely to appear, and can be fixed by tweaking the name of the dynamic argument. This should be more efficient, as we did compare equal strings each time. | |||
| 2013-11-21 | configure: CAML_LD_LIBRARY_PATH is enriched, not overwritten | Pierre Letouzey | |
| Keeping the earlier content of this variable is crucial for opam (at least). Thanks to François Bobot and Thomas Refis for this one... | |||
| 2013-11-21 | configure: fix some issues with last commit | Pierre Letouzey | |
| - after piping with | tr -d, an exit code was lost - suspicious use of " " inside a larger " ", we use ' ' now instead | |||
| 2013-11-21 | Fix various \r issues with windows | Jason Gross | |
| Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153. | |||
| 2013-11-21 | Field_theory: nicer notations for constants 0 1 ... | Pierre Letouzey | |
| 2013-11-21 | updated .mailmap | Pierre Letouzey | |
| 2013-11-21 | Add Acc_intro_generator on top of all wf function proof (much much faster ↵ | Julien Forest | |
| execution) | |||
| 2013-11-20 | Adding Acc_intro_generator in order to help computations of Function in ↵ | forest | |
| particular | |||
| 2013-11-19 | Optimization: in case of empty substitution, merging is trivial. | Pierre-Marie Pédrot | |
| 2013-11-19 | update .mailmap with my email now that I've used it in a commit | Pierre Letouzey | |
| 2013-11-19 | A .mailmap file for a nice git-shorlog display | Pierre Letouzey | |
| In particular, this file allows to merge duplicated identities of a same person. See man git shortlog for more details. | |||
| 2013-11-18 | A file listing old svn branches and tags | letouzey | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17095 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-11-16 | Slightly faster version of merging substitutions in TacticMatching. | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |