aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Collapse)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
| | | | | | | | - Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
| | | | | | | | | | | | agreement with wish #2117 (pattern unification of evars remained deactivated for 3 years because of incompatibilities with eauto [see commit 9234]; thanks to unification flags, it can be activated for apply w/o changing eauto). Also add test for bug #2123 (see commit 12228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
| | | | | | | rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12158 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
| | | | | | | | | | revealed a too strict test for detection of inferable metas in Clenv. Restored tolerance for unbound names in interactive tactic use. - Moral removals of some captures of Not_found in Environ.evaluable_* since kernel is assumed to deal with existing names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
| | | | | | | | | | - Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
| | | | | | | | | | | to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
| | | | | | | | | | | Not_found bug in Theorem with) from V8.2 to trunk. - Improving indentation in presence of tabulation and utf-8 when reporting error messages with "^^^^^^". - Updating a few svn:ignore properties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
| | | | | | | | {measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
| | | | | | | | | | | | | | | - The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ↵Gravatar barras2009-03-19
| | | | | | genargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
| | | | | | | | | | | | | | now works correctly, "unfold foo at 4 in H at 3" now fails correctly, etc.). The terminology for clauses (though I don't find the term "clause" very intuitive after all) is mostly preserved except for "simple_clause" which becomes a light form of "clause" instead of being an atom of clause (what played the role of "simple_clause" is now called "goal_location" - better names are welcome). Main changes are in tacticals.ml and tactics.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
* From v8.2 to trunk:Gravatar herbelin2009-02-06
| | | | | | | | | - commit 11871 (Miller's pattern detection bug) + a corresponding test - commit 11883 (.ml4 to .cmxs in coq_makefile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
| | | | | | | [dependent induction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
| | | | | | | scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
| | | | | | | | | late 2008 Coq WG. - Updated Copyright file wrt JProver. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
| | | | | | | | | | variant of the [unify] tactic that takes a hint db as argument and does unification modulo its [transparent_state]. Add test-file for bug #1939 and another [AdvancedTypeClasses.v] that mimicks [AdvancedCanonicalStructure.v]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for syntax changes in test-suite scripts.Gravatar msozeau2008-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11684 85f007b7-540e-0410-9357-904b9bb8a0f7
* About "apply in":Gravatar herbelin2008-12-09
| | | | | | | | | | | | | | | | | | - Added "simple apply in" (cf wish 1917) + conversion and descent under conjunction + contraction of useless beta-redex in "apply in" + support for open terms. - Did not solve the "problem" that "apply in" generates a let-in which is type-checked using a kernel conversion in the opposite side of what the proof indicated (hence leading to a potential unexpected penalty at Qed time). - When applyng a sequence of lemmas, it would have been nice to allow temporary evars as intermediate steps but this was too long to implement. Smoother API in tactics.mli for assert_by/assert_as/pose_proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved simplGravatar barras2008-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new directory for pre-compilation of files needed for further tests.Gravatar herbelin2008-12-02
| | | | | | | Application to the test of notation import from within a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
* added tests for hyps reorderingGravatar barras2008-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11635 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction erreur dans test output Notation.vGravatar herbelin2008-11-09
| | | | | | | - Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
| | | | | | | | | | | | | | | | | help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add some example uses of the new record features in Record.v:Gravatar msozeau2008-11-07
| | | | | | | | | | | | - introduction notation with missing fields and interaction with Program. - Ability to add (currently a single) "where notation" clause to each field. - Use every information available to do type inference and internalisation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
| | | | | | | | given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
| | | | | | | Grant wish #1988 ("fun" forces reduction in "refine" if needed) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
| | | | | | | | | s'est avéré ralentir la compilation des user-contribs au final, sans compter aussi le bug 1980 apparemment introduit par ce commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | | - New constr_expr construct [CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr] to generalize the free vars of the [constr_expr], binding these using [binding_kind] and making a lambda or a pi (or deciding from the scope) using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) - Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for implicit bindings (both "..(" and "_(" seem much more difficult to implement). Subject to discussion! A few examples added in a test-suite file. - Also add missing syntax for implicit/explicit combinations for _binders_: "{( )}" means implicit for the generalized (outer) vars, explicit for the (inner) variable itself. Subject to discussion as well :) - Factor much typeclass instance declaration code. We now just have to force generalization of the term after the : in instance declarations. One more step to using Instance for records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
| | | | | | | | | | | | | | | | | | dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci dit : - cela ne me parait pas moral que clos_norm_flags s'occupe de normaliser les evars, - mais comme "evar" n'est pas un flag supporté par closure.ml, on ne peut pas le donner à la demande comme argument de clos_norm_flags (question: pourrait-on faire supporter la réduction Evar par closure.ml ??). Plus généralement, il y a un problème avec la propagation des instantiations des evars à travers les buts (cf lemme eapply_evar dans test-suite/success/apply.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11470 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
| | | | | | | | | - Makefile: typo apparente avec .ml4.preprocessed - test-suite: ajout d'un test sur eta qui trainait dans le coin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11465 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: more utf8 tests, a test of ! ? and so on in rewritesGravatar letouzey2008-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
| | | | | | | induction test-suite script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
| | | | | | | | | | | - Do not touch at the user equalities and so on by using a blocking constant. This avoids the wild autoinjections and subst tactics that were used before. Thanks to Brian Aydemir for an example were this hurt a lot. - Debug the tactic used to simplify induction hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
| | | | | | | | | | dance when defining a new program by default, which forces use of JMeq but makes for much more robust tactics. Everything in success/Equations works except for limitations due to JMeq or the guardness checker (one example seems to actually diverge...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
| | | | | | | | | when one wants a particular type. Rewrite of the unification behind [Equations], much more robust but still buggy w.r.t. inaccessible patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
| | | | | | | simplifications (homogeneous equations first). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more debugging of [Equations], unification still not perfect.Gravatar msozeau2008-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11396 85f007b7-540e-0410-9357-904b9bb8a0f7
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
| | | | | | | | dependent [noConfusion] definitions in "A Few Constructions on Constructors". Now the guardness check is blocking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
| | | | | | | | support for "where" notation declarations as well. Better checking of recursivity or not, after type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
| | | | | | | | definition is recursive or not based on occurence of a rec call in the body. Examples updated, enjoy! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11353 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 15:43:36 +0000