aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-11Other bugs with "inversion as" (collision between user-provided names and ↵Hugo Herbelin
generated equation names).
2014-09-11Fix bug #3594: eta for constructors and functions at the same time whichMatthieu Sozeau
was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
2014-09-11Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Matthieu Sozeau
2014-09-11Fix bug #3505.Matthieu Sozeau
When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type).
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
implicits do not allow to parse as an application and cleanup code.
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
2014-09-10Example for apply and evars.Hugo Herbelin
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
2014-09-08Fixing TestRefine test-suite file.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
use of projections.
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
2014-09-04Add test-suite file for Case derivation on primitive records.Matthieu Sozeau
2014-09-04Add test suite files for closed bugs.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object.
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-03Test-suite for bug #2818.Pierre-Marie Pédrot
2014-09-02Adding a test-suite for second-order matching order and indexes.Pierre-Marie Pédrot
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
fresh names interferring with names later generated in intropatterns (as introduced in 72498d6d68ac which passed "clenv_refine_in continued by pattern introduction" to descend_in_conjunction while only a pure clenv_refine was passed before). The 72498d6d68ac version was generating fresh names in the wrong order (morally-private names for descend_in_conjunction before user-level names in clenv_refine_in). The 19a7a5789c fix was introducing expressions not handled by the refine from logic.ml. In particular, this fixes RelationAlgebra.
2014-09-02An apply test.Hugo Herbelin
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
2014-08-29Not using a "cut" in descend_in_conjunctions induced more success. WeHugo Herbelin
at least remove the successes obtained by trivial unification of a meta with the goal, so as to avoid surprising results. We generalize this to variables which will only eventually be replaced by metas.
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
eta-expanded version of a projection as before.
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
The unification oracle now prefers unfolding the eta-expanded form of a projection over the primitive projection, and allows first-order unification on applications of constructors of primitive records, in case eta-conversion fails (disabled by previous patch on eta).
2014-08-28There are some occurs-check cases that can be handled by imitation (using ↵Matthieu Sozeau
pruning), hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
presence of let-ins.
2014-08-28Adding test-suite for bug #3212.Pierre-Marie Pédrot
2014-08-26Add a regression test for 3427Jason Gross
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-25Fixing a bug introduced in the extension of 'apply in' + simplifying code.Hugo Herbelin
2014-08-23Fix test-suite file.Matthieu Sozeau
2014-08-18Fixing unification of subterms identified by patterns.Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine).
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-18Fix test-suite files.Matthieu Sozeau
2014-08-18Fix test-suite file.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 11:12:06 +0000