aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
| | | | | | | | | | | setoid rewrite. Refine and use the new unification flags setup by Hugo to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean indicating conversion is wanted to a Cpred representing the constants one wants to get unfolded to have more precise control. Add corresponding test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cible programs comme synonyme de subtacGravatar herbelin2008-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc: Add test for bug 1704, now closed. Add usual syntax for lists inGravatar msozeau2008-03-16
| | | | | | | | Program.Syntax along with stronger implicits. Update dependent induction test file using unicode syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
| | | | | | | | | | | | implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes on setoid rewriting. Now uses definitions of [relation] andGravatar msozeau2008-03-16
| | | | | | | | [id] instead of their expansions. Seems to slow things down a bit (1s. on Ring_polynom). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)Gravatar letouzey2008-03-15
| | | | | | | | | | | | | | | | | | | * FSetAVL is greatly lightened : modulo a minor change in bal, formal proofs of avl invariant is not needed for building a functor implementing FSetInterface.S (even if this invariant is still true) * Non-structural functions (union, subset, compare, equal) are transformed into efficient structural versions * Both proofs of avl preservation and non-structural functions are moved to a new file FSetFullAVL, that can be ignored by the average user. Same for FMapAVL (still work in progress...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot the test file.Gravatar msozeau2008-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
| | | | | | | | | | | | | | | | | | works in inductive type definitions and fixpoints. The semantics of an implicit inductive parameter is maybe a bit weird: it is implicit in the inductive definition of constructors and the contructor types but not in the inductive type itself (ie. to model the fact that one rarely wants A in vector A n to be implicit but in vnil yes). Example in test-suite/ Also, correct the handling of the implicit arguments across sections. Every definition which had no explicitely given implicit arguments was treated as if we asked to do global automatic implicit arguments on section closing. Hence some arguments were given implicit status for no apparent reason. Also correct and test the parsing rule which disambiguates between {wf ..} and {A ..}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapt funind to the RLetPattern constructor.Gravatar msozeau2008-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur le test censé discriminer entre une erreur d'evar nonGravatar herbelin2008-03-15
| | | | | | | | | | résolue et une anomalie. Il ne marche pas. La question de trouver la bonne manière de tester qu'un exemple renvoie une erreur (non rattrapable par tactique) et une anomalie reste ouverte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
| | | | | | | | | | | | | appels à type_of et get_type_of sont souvent utilisés pour construire des termes à partir de types; on ne rajoute pas non plus de contraintes inutiles parce que type_of et get_type_of ne changent pas le graphe de contraintes; tout ce qu'on perd est une information utilisateur sur le type en lui-même mais puisque pretty.ml n'appelle ni type_of ni get_type_of, ces informations sur la représentation interne des univers restent a priori accessibles pour l'utilisateur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppress some warnings by writing ugly Coq.Relations.Relations in some .vGravatar letouzey2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10672 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid universe problems with pf_get_type in f_equalGravatar letouzey2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10670 85f007b7-540e-0410-9357-904b9bb8a0f7
* New option -glob for coqdep, in order to avoid nasty tricks with sed in MakefileGravatar letouzey2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack wrong commit.Gravatar courtieu2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10667 85f007b7-540e-0410-9357-904b9bb8a0f7
* kill a warning (and clean the code around)Gravatar letouzey2008-03-14
| | | | | | | | | ... After sending a "yakafokon" email, let's start a code-cleanup session... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10666 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage de code obsolete.Gravatar soubiran2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10664 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique gappaGravatar filliatr2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10663 85f007b7-540e-0410-9357-904b9bb8a0f7
* indentation.Gravatar courtieu2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10662 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix the 'decreasing on Xth' messageGravatar letouzey2008-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10661 85f007b7-540e-0410-9357-904b9bb8a0f7
* trying fGravatar courtieu2008-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10659 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Catching a Not_found exception when trying to use Scheme Equality Gravatar vsiles2008-03-12
| | | | | | | over inductives types using Parameters git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10658 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique Gappa : mise en placeGravatar filliatr2008-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forget to update the CHANGES file after the commit r10180Gravatar vsiles2008-03-11
| | | | | | | | (about the Scheme Equality mechanism) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10656 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique Gappa : mise en placeGravatar filliatr2008-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo commit 10653Gravatar herbelin2008-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas très propre de reposer sur la capture des anomalies (et celaGravatar herbelin2008-03-10
| | | | | | | | | complique le débogage...). Réécriture de 2 morceaux de code qui utilisaient les anomalies à des fins détournées de leur intention. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10653 85f007b7-540e-0410-9357-904b9bb8a0f7
* fold travaille maintenant sur la forme beta-iota-zeta réduite duGravatar herbelin2008-03-10
| | | | | | | | | corps de la constante (comme unfold le fait ici), de telle sorte que "unfold f; fold f" marche (cf bug 1789) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indexation de pose proof, et par la même occasion du nouveau specializeGravatar herbelin2008-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
| | | | | | | | | - Correction bug des filtres dans define_evar_as_abstraction - Nettoyage, documentation et réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation problem and finish little cleanup.Gravatar msozeau2008-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a missing morphism declaration that turns morphisms on R ==> R' toGravatar msozeau2008-03-09
| | | | | | | | | morphisms on R --> inverse R' for any R, R' (report by N. Tabareau). Better implementation of unfolding for impl that does it only where necessary to keep the goal in the same shape as the user gave. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a few bugs in Program: use user-given typing constraints forGravatar msozeau2008-03-09
| | | | | | | | constant declarations, correct coercion between dependent products. Remove fragile inh_conv_coerces_to code, may break existing Programs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des choses bizarres avec pa_op.cmo (extension syntaxique pour parser)Gravatar herbelin2008-03-09
| | | | | | | | | | | | se passent avec camlp5 qui ne se passaient pas avec l'ancien camlp4: pa_op.cmo exige camlp5o.cma mais alors, il y a un message de redéfinition de ipatt que je ne sais pas éviter avec coqtop.byte. Puisque pa_op.cmo n'est finalement pas utile, on le retire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10646 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of Add Relation as a DefaultRelation instanceGravatar msozeau2008-03-08
| | | | | | | | declaration. Really fix bug#1704, correct order of condition subgoals even in setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10642 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)Gravatar jforest2008-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
| | | | | | | | | | | | | | | | | | implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile : backtrack sur les liens vers les exécutables ocamlGravatar notin2008-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10638 85f007b7-540e-0410-9357-904b9bb8a0f7
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * "f_equal" is now a tactic in ML (placed alongside congruence since it uses it). Normally, it should be completely compatible with the former Ltac version, except that it doesn't suffer anymore from the "up to 5 args" earlier limitation. * "revert" also becomes an ML tactic. This doesn't bring any real improvement, just some more uniformity with clear and generalize. * The experimental "narrow" tactic is removed from Tactics.v, and replaced by an evolution of the old & undocumented "specialize" ML tactic: - when specialize is called on an hyp H, the specialization is now done in place on H. For instance "specialize (H t u v)" removes the three leading forall of H and intantiates them by t u and v. - otherwise specialize still works as before (i.e. as a kind of generalize). See the RefMan and test-suite/accept/specialize.v for more infos. Btw, specialize can still accept an optional number for specifying how many premises to instantiate. This number should normally be useless now (some autodetection mecanism added). Hence this feature is left undocumented. For the happy few still using specialize in the old manner, beware of the slight incompatibities... * finally, "contradict" is left as Ltac in Tactics.v, but it has now a better shape (accepts unfolded nots and/or things in Type), and also some documentation in the RefMan git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10637 85f007b7-540e-0410-9357-904b9bb8a0f7
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10636 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
| | | | | | | | | of the fix I added an optional "by" annotation for rewrite to solve said conditions in the same tactic call. Most of the theories have been updated, only FSets is missing, Pierre will take care of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de coq_makefileGravatar notin2008-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10633 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo in last commit (?)Gravatar letouzey2008-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coquille vraisemblablement introduite par la révision 10628Gravatar notin2008-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10630 85f007b7-540e-0410-9357-904b9bb8a0f7
* repair for commit 10612 (due to grammar order, some syntaxes weren't working) Gravatar letouzey2008-03-06
| | | | | | | | | and add a simpler synonym for "exactly N times" : rewrite 3 H (or rewrite 3H) means rewrite 3!H git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | | binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Toujours suite commits 10623 et 10624:Gravatar herbelin2008-03-06
| | | | | | | | | | - l'occur-check doit être fait aussi quand on imite, - pour simplifier et en se basant sur les commentaires antérieurs à 1995 (de Chet?) et parlant de mimick_evar, on restreint l'appel à mimick_evar au cas où l'instance contient des Meta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10626 85f007b7-540e-0410-9357-904b9bb8a0f7
* even_2n et odd_S2n deviennent transparents (chez moi, ça empêchait de ↵Gravatar notin2008-03-06
| | | | | | compiler la contrib Nijmegen/QArith ?!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10625 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:38:16 +0000