aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Suite commit 10623:Gravatar herbelin2008-03-06
| | | | | | | | | | - les erreurs de solve_simple_evar_eqn étaient rattrapées par mégarde, - à défaut de traitement des conv_pbs dans unification.ml, on évite d'accumuler des contraintes pour l'instant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nGravatar herbelin2008-03-06
| | | | | | | | | dans certains cas. Branchement au passage de w_unify vers evar_conv et solve_simple_eqn en cas d'équations entre Evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une typo restant du commit 10557 et cause d'échec de contribsGravatar herbelin2008-03-05
| | | | | | | | telles que Godel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la révision #10401 : suppression de le_minus de la base de ↵Gravatar notin2008-03-05
| | | | | | hints arith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt of fix for extraction of modules typesGravatar letouzey2008-03-05
| | | | | | | | | | | | | | | | | * When no explicit module type is given in Coq, extraction proceeds with more caution when recontructing a module type from the module. For instance, a module ident isn't keep, since it's the name of an implementation, not of a module type. Fix the bug functor M -> M : funsig M -> M instead of funsig M -> typeof(M) * Removed duplicated code with Modops * The call to replicate_msid doesn't seem to be as crucial as before. Let's try to remove it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement de l'auto-save de coqide par défautGravatar herbelin2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10619 85f007b7-540e-0410-9357-904b9bb8a0f7
* still one more substituion s/Set/Type/Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10618 85f007b7-540e-0410-9357-904b9bb8a0f7
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
* use loc instead of dummy_loc in the ugly intro-pattern rewrite hackGravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10615 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)Gravatar letouzey2008-03-02
| | | | | | | | | ... but still no idea why it was working fine on some machines even without this patch... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_OGravatar herbelin2008-03-01
| | | | | | | | (rapport de bug 1807). Cf explication dans le fichier et/ou dans le bug-tracker. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1) changed the semantics of rewrite H,H' : the earlier semantics (rewrite H,H' == rewrite H; rewrite H') was poorly suited for situations where first rewrite H generates side-conditions. New semantics is tclTHENFIRST instead of tclTHEN, that is side-conditions are left untouched. Note to myself: check if side-effect-come-first bug of setoid rewrite is still alive, and do something if yes 2) new syntax for rewriting something many times. This syntax is shamelessly taken from ssreflect: rewrite ?H means "H as many times as possible" (i.e. almost repeat rewrite H, except that possible side-conditions are left apart as in 1) rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H) rewrite 3?H means "up to 3 times", maybe less (i.e. something like: do 3 (try rewrite H)). rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H). For instance: rewrite 3?foo, <-2!bar in H1,H2|-* 3) By the way, for a try, I've enabled the syntax +/- as synonyms for ->/<- in the orientation of rewrite. Comments welcome ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite modif pour pouvoir faire "intros until 0" qui introduit autant Gravatar aspiwack2008-02-29
| | | | | | | | | | que possible des variables qui ont déjà un nom joli tout plein. La conséquence c'est qu'on peut aussi faire "destruct 0" qui est vachement moins intéressant... Mais bon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argumentation plus poussée de pourquoi on retire la condition x>0 dansGravatar herbelin2008-02-29
| | | | | | | | | Rpower_O alors qu'on la garde pour les autres propriétés de la puissance. (résultat d'une discussion avec Assia et Jean-Marc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some suggestions about FMap by P. Casteran: Gravatar letouzey2008-02-28
| | | | | | | | | | | | - clarifications about Equality on maps Caveat: name change, what used to be Equal is now Equivb - the prefered equality predicate (the new Equal) is declared a setoid equality, along with several morphisms - beginning of a filter/for_all/exists_/partition section in FMapFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: correction de l'appel aux exécutables OcamlGravatar notin2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Correction d'un bug sur les options passées à CoqdocGravatar notin2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not open type_scope in SetoidClass.Gravatar msozeau2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation problem (hopefully).Gravatar msozeau2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer third spec of choose. Gravatar letouzey2008-02-28
| | | | | | | | The old version is now a properties in FSetProperties.OrdProperties git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
* For more uniformity, use implicits in FSetAVLGravatar letouzey2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10600 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 02:42:05 +0000