aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
| | | | | | | | | | | | | corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
* Moving the ML tactic extension mechanism to a Libobject-based one.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Plugin names must be declared in the header of .ml4 file, be they static orGravatar Pierre-Marie Pédrot2014-05-12
| | | | dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
* Adding the possibility for ML modules to declare functions to be called atGravatar Pierre-Marie Pédrot2014-05-12
| | | | | caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins.
* Fixing the undocumented -dumpgraphbox option of coqdep.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
| | | | and the lookup operation proved to be costly when dealing with big libraries.
* Eliminating a potentially quadratic behaviour in Require, by using mapsGravatar Pierre-Marie Pédrot2014-05-11
| | | | instead of lists to test if a library has already been encountered.
* Add appropriate Fail(s) to opened bugsGravatar Jason Gross2014-05-10
| | | | | | | | The contract is that a file in bugs/opened should not raise errors if the bug is still open. Some of them fail for different reasons than they used to; I'm not sure what to do about these.
* Move opened bugs to bugs/openedGravatar Jason Gross2014-05-10
|
* Add more regression tests for univ poly/prim projGravatar Jason Gross2014-05-10
| | | | | | | | | | | hese regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently fails. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
|
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
|
* More documentation of new features in CHANGE.Gravatar Pierre-Marie Pédrot2014-05-09
|
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
| | | | fixing two opened bugs from HoTT/coq.
* Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2014-05-09
|\ | | | | | | into JasonGross-working-polyproj-tests
* | Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
| | | | | | | | | | abstraction has the right type. Fixes bug# 3306. Add test-suite files for bugs 3305 and 3306.
* | Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
| |
* | Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
| | | | | | | | problem with hashconsing at the same time. This fixes bug# 3302.
* | Encapsulating some clausenv uses. This simplifies the control flow of someGravatar Pierre-Marie Pédrot2014-05-08
| | | | | | | | tactics.
* | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
| | | | | | | | | | | | | | (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.
* | Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
| |
* | Typo reference manualGravatar Hugo Herbelin2014-05-08
| |
* | Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
| | | | | | | | which compute an abstraction of the goal over a term or a pattern.
* | Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
| | | | | | | | | | works in the presence of local definitions referring to x and dependent in other hyps or concl.
* | Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
| |
* | Little reorganization of generalize tactics code w/o semantic changes.Gravatar Hugo Herbelin2014-05-08
| | | | | | | | Also removing trailing spaces.
* | Cleanup code in pretyping/evarutilGravatar Matthieu Sozeau2014-05-08
| |
* | Fix performance problem with unification in presence of universes (bug ↵Gravatar Matthieu Sozeau2014-05-08
| | | | | | | | | | | | | | #3302) by considering Type i a ground term even when "i" is a flexible universe variable, using the infer_conv function to do the unification of universes.
* | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵Gravatar Matthieu Sozeau2014-05-08
| | | | | | | | | | | | | | | | evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet).
* | Avoid allocations in type_of_inductiveGravatar Matthieu Sozeau2014-05-08
| |
* | Fast-path equality of sorts in compare_constr*Gravatar Matthieu Sozeau2014-05-08
| |
* | Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
| |
* | Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
| |
* | Fixing test-suite for bug #3043.Gravatar Pierre-Marie Pédrot2014-05-08
| |
* | Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
| | | | | | | | shows the polymorphism status of the term.
* | Code cleaning in Tacinterp: factorizing some uses of tclEVARS.Gravatar Pierre-Marie Pédrot2014-05-08
| |
* | Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
| | | | | | | | answers #3299).
* | Adding test-suite for bug #3242.Gravatar Pierre-Marie Pédrot2014-05-06
| |
| * Add regression tests for univ. poly. and prim projGravatar Jason Gross2014-05-06
|/ | | | | | | | | | These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.
* Remove Lemmas from base_include, it's not linked in dev/printers anymoreGravatar Matthieu Sozeau2014-05-06
|
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
|
* Use new tactic combinators in tclABSTRACT, to avoid blowup when using ↵Gravatar Matthieu Sozeau2014-05-06
| | | | | | V82.tactic (tclEVARS _). Again, performance is back to normal. Remove reintroduced try .. with _ -> in raw_enter's.
* Add missing case for primitive projection in fold_map.Gravatar Matthieu Sozeau2014-05-06
|
* Fix after merge.Gravatar Matthieu Sozeau2014-05-06
|
* Add incompatibilities paragraph in doc about universe polymorphism.Gravatar Matthieu Sozeau2014-05-06
|
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
| | | | | | | | | in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. - Fix a HUGE performance problem in the processing of constraints, which was remerging all the previous constraints with the ambient global universes at each new constraint addition. Performance is now back to (or better than) normal.
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
| | | | | Fix restriction of universe contexts to not forget about potentially useful constraints.
* Fix Field_tac to get fast reification again, with the fix on template ↵Gravatar Matthieu Sozeau2014-05-06
| | | | universe polymorphic constructors.
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
| | | | | | | eagerly solve l <= k constraints as k := l when k is a fresh variable coming from a template type. This has the effect of fixing the variable at the first instantiation of the parameters of template polymorphic inductive and avoiding to generate useless <= constraints that need to be minimized afterwards.
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 04:18:41 +0000