aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2008-06-08Second pass on typeclasses documentation, fix html rendering.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11070 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Fix library index template and associated script.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11067 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t))) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01remove additional occurrences of +/- forgotten in commit 11030letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11032 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'àherbelin
peine plus courts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11030 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
impossibles dans un filtrage dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Fix bashism in doc generation.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10986 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10979 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23Nouvelle doc pour les modules.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10974 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Strategy commands are now exportedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21refined the conversion oraclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19MAJ créditsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-13- Fix bug related to indices of fixpoints.msozeau
- Add a typeclasses_eauto which uses only the typeclass_instances database. - Set obligations as transparent by default to avoid the common problem with ill-formed recursive defs due to opaque obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10925 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12MAJ et bricoles diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
change the default pretty-printing to use Π, λ instead of forall and fun (and allow "," as well as "=>" for "fun" to be more consistent with the standard forall and exists syntax). Parsing allows theses new forms too, even if not in -unicode, and does not make Π or λ keywords. As usual, criticism and suggestions are welcome :) Not sure what to do about "->"/"→" ? - [setoid_replace by] now uses tactic3() to get the right parsing level for tactics. - Type class [Instance] names are now mandatory. - Document [rewrite at/by] and fix parsing of occs to support their combination. - Backtrack on [Enriching] modifier, now used exclusively in the implementation of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06[ring] constructor for power was missing in the docbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10891 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-05Minor updates in the documentation of notations.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10886 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-29Fix eauto still using delta when it shouldn't (should make CoRN compilemsozeau
in reasonable time), add (unfinished) documentation on type classes. Put some classes into Prop explicitely as singleton inductive types are no longer in Prop by default even if all the arguments are (is that really what we want? roconnor says no). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-26Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour herbelin
"set (f:=fun n => t)" (et idem pour pose). Documentation notation Record sans sort et, en passant, "let|" -> "let '". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10852 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21Correction bug 1838 + doc modules.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10821 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-17documentation tactique gappafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10809 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-17Add almost empty Classes.tex for documentation of type classes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10808 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
SetoidTactics and document it. Cleanup Classes.Equivalence. Minor fixes to the Program doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10799 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15* added a subsection to explain the automatic declaration of schemes:vsiles
* Set\Unset Elimination Schemes to switch on/off the declaration of standard elimination schemes * Set\Unset Equality Scheme to switch on/off the declaration of the boolean equality * added a \Rem in injection to explain that if we managed to get a boolean equality, injection can finally work well with dependant pairs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10798 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
- Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15typovsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10795 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Update doc and remove another overloading of equiv_*.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10788 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
testing: - better? pretty printing - correct handling of load/open/cache - do less reduction in build_signature, commited in previous patch. May break some scripts (but Parametric will break more and before :). - remove ===def notation as suggested by A. Spiwack. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10783 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Chgts mineurs:herbelin
- correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
to reduce proofs (requested by users). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23Fix examples in Program documentation and add comindexes for the variousmsozeau
commands. Update documentation of implicit arguments with the new syntax and an explanation for the way it works in inductive type definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10714 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19some references to IntMap forgotten in last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10700 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19migration of the old IntMap library from StdLib to a user contrib ↵letouzey
(Cachan/IntMap) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-10Indexation de pose proof, et par la même occasion du nouveau specializeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10651 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
* "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
2008-03-06repair for commit 10612 (due to grammar order, some syntaxes weren't working) letouzey
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
2008-03-01Rework on rich forms of rewriteletouzey
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
2008-02-27Bug dans la génération de la stdlibnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10595 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Plongement de doc/Makefile dans la nouvelle architecutre des Makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Suppression de l'option -glob-from de Coqdoc: les globalisations sontnotin
lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Documentation of CHANGES and refman doc for the implicit argument bindermsozeau
`X`. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10538 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08New "Preterm [ of id ] " command to show the preterm before giving it tomsozeau
Coq (solves part 2 of bug #1784). Add corresponding documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08updates concerning FSetsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10527 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 02:15:39 +0000