aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Test suite: update output reference.Gravatar xclerc2013-12-02
|
* Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into ↵Gravatar xclerc2013-12-02
|\ | | | | | | trunk
* | Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
| |
| * Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
| |
| * Ensuring the right parsing of glob arguments, used by refineGravatar Pierre-Marie Pédrot2013-12-01
| | | | | | | | | | | | | | | | and instantiate. Each of these tactics uses it at a different parsing level, thus actually triggering a parsing error after merging them. This fix implies some code duplication, which is a pity. The separation between genargs and parsing entries should be made one day.
| * Fixing ltac constr variable handling in refine.Gravatar Pierre-Marie Pédrot2013-11-30
| |
| * Adding printing of ltac envs to debugger.Gravatar Pierre-Marie Pédrot2013-11-30
| |
| * Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
| * Better heuristic for name generation backward compatibility. We fallbackGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | to old behaviour whenever we were in Program mode.
| * Useless instantiation function exported in Evd.Gravatar Pierre-Marie Pédrot2013-11-30
| |
| * Tentative fix to recover fresh name generation as it was beforeGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | | | | | 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.
| * First stab at documenting Canonical StructuresGravatar Enrico Tassi2013-11-29
| |
| * Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notGravatar Hugo Herbelin2013-11-29
|/ | | | | | | | 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...
* Testsuite: flatten the 'bugs/opened' directory.Gravatar xclerc2013-11-29
|
* Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)Gravatar xclerc2013-11-28
|
* Getting rid of goal-dependency in declarative mode argument evaluation.Gravatar Pierre-Marie Pédrot2013-11-27
|
* Fixing abstract tactic by using a dummy name out of a declared proof.Gravatar Pierre-Marie Pédrot2013-11-27
|
* Actually adding the grammar entry to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
|
* Adding the necessary hooks to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
|
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Old message Interp returns the state id so that one can BackTo itGravatar Enrico Tassi2013-11-27
|
* New option --help-XML-protocol to document the XML procol used by -ideslaveGravatar Enrico Tassi2013-11-27
| | | | | | 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.
* First stab at retrocompatible INTERP messageGravatar Enrico Tassi2013-11-27
|
* Use my real email address in .mailmapGravatar Enrico Tassi2013-11-27
|
* Reduction: every n iterations a slaves process checks for interruptionGravatar Enrico Tassi2013-11-27
| | | | | | | 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.
* STM: restart slave after every proofGravatar Enrico Tassi2013-11-27
| | | | | | | | 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.
* CoqIDE: show error message for parsing errorsGravatar Enrico Tassi2013-11-27
|
* Adding a generic Int.Map using persistent arrays.Gravatar Pierre-Marie Pédrot2013-11-26
|
* Do not use ugly Dyn features in the Quote plugin. Use instead theGravatar Pierre-Marie Pédrot2013-11-26
| | | | provided tactic environment to handle open terms.
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
| | | | | | | | 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.
* Factoring: is_section_variable.Gravatar Arnaud Spiwack2013-11-25
| | | | In 0c7a77, I inadvertantly re-defined an is_section_variable function.
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
| | | | | | 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.
* Typo resulting in bad eta-expansion of destructing let's body.Gravatar Hugo Herbelin2013-11-25
| | | | Revealed by message on coq-club on 24/11/2013.
* Better implementation of summary unfreezing.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Adding fold_left / fold_right function to maps.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Updating new ftp link to old archives.Gravatar Hugo Herbelin2013-11-24
|
* Hardening the reading function of vo files.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Slightly more efficient zip function in Closure.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Tweaking arity & allocation of some basic functions.Gravatar Pierre-Marie Pédrot2013-11-24
|
* Small allocation improvement in Closure.Gravatar Pierre-Marie Pédrot2013-11-23
|
* configure: typo in my last commitGravatar Pierre Letouzey2013-11-23
|
* Fixing bug #3165.Gravatar Pierre-Marie Pédrot2013-11-23
|
* Remove some occurrences of obsolete operatorsGravatar Stephane Glondu2013-11-22
|
* configure: improve last fixGravatar Pierre Letouzey2013-11-22
| | | | | | | | | | 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
* Using hashes in Summary, like the previous commit did with Dyn.Gravatar Pierre-Marie Pédrot2013-11-22
|
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
| | | | | | | | 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.
* configure: CAML_LD_LIBRARY_PATH is enriched, not overwrittenGravatar Pierre Letouzey2013-11-21
| | | | | | | Keeping the earlier content of this variable is crucial for opam (at least). Thanks to François Bobot and Thomas Refis for this one...
* configure: fix some issues with last commitGravatar Pierre Letouzey2013-11-21
| | | | | - after piping with | tr -d, an exit code was lost - suspicious use of " " inside a larger " ", we use ' ' now instead
* Fix various \r issues with windowsGravatar Jason Gross2013-11-21
| | | | | | Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153.
* Field_theory: nicer notations for constants 0 1 ...Gravatar Pierre Letouzey2013-11-21
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 14:25:04 +0000