aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Collapse)Author
2009-03-14Coqdep: remove references to obsolete .zi and Require Implementation stuffletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-04doc et CHANGES pour la commande Timeoutbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11962 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Modification du style du manuel de référencenotin
(cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-27- Fixed various Overfull in documentation.herbelin
- Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fixes in the documentation of [dependent induction] and test-suitemsozeau
scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Added some missing statements for proof folding and correctedvgross
the reference manual accordingly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11815 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Added proof folding into CoqIde. See RefMan for using it.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11814 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- 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
2009-01-18Last changes in type class syntax: msozeau
- curly braces mandatory for record class instances - no mention of the unique method for definitional class instances Turning a record or definition into a class is mostly a matter of changing the keywords to 'Class' and 'Instance' now. Documentation reflects these changes, and was checked once more along with setoid_rewrite's and Program's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Updated datesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
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
2009-01-08Minor doc fixes:msozeau
- Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-03Fixed two problems:herbelin
- Function descend_in_conjunctions was now too weak, use match_with_record. - Added documentation of new notation for destruct with equation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11742 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-01- Fixed bug #2021 (uncaught exception with injection/discriminate whenherbelin
the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-14Fixes in the type classes documentation:msozeau
- Document the new binders, now in sync with the implementation - Fix the examples - Redo the part about superclasses now that we got rid of "=>" - Add explanation of singleton "definitional" classes - Add info about the optional priority attribute of instances (thanks to M. Lasson for pointing it out). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11680 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-09About "apply in":herbelin
- 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
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11642 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Fix typo in omega docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Document native "Declare ML Module"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-27- Fixed many "Theorem with" bugs.herbelin
- Fixed doc of assert as. - Doc of apply in + update credits. - Nettoyage partiel de Even.v en utilisant "Theorem with". - Added check that name is not in use for "generalize as". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-24Fix doc of apply in (see coq-club message 26 September 2008)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11499 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-20Renommage "Global Instance" en "Instance Global" pour uniformisationherbelin
de l'utilisation des modificateurs Global/Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11480 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
- Extension du test de réversibilité acyclique des notations dures aux notations de type abbréviation (du genre inhabited A := A). - Ajout options Local/Global à Transparent/Opaque. - Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé dependent retiré). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-14report de la révision r11451 (nouveau style html pour le manuel de référence)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11452 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
SearchAbout + referring objects by their notation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-14A pass on documentation: msozeau
- Don't use [Eq] and [eq] in the typeclasses documentation, as advised by Assia. - Explain the importance of [Transparent/Opaque] for typeclasses and [setoid_rewrite]. - Fix and rework doc on [dependent induction]. - A word on [Global] instance. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11410 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
[discriminated]] with a switch for using the more experimantal dnet impl for every hint. Also add [Hint Transparent/Opaque] which parameterize the dnet and the unification flags used by auto/eauto with a particular database. Document all this. Remove [Typeclasses unfold] directives that are no longer needed (everything is unfoldable by default) and move to [Typeclasses Transparent/Opaque] syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-06correction : coqart is already publishedjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11307 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Évolutions diverses et variées.herbelin
- Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-29Typo in docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11292 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-23Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theherbelin
opportunity to extend the class of singleton types to (possibly mutual) recursive types with single constructors of which all arguments are in Prop. This covers Acc. Acc_rect can consequently be defined in the direct way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18- Rebranchement backtrack du langage déclaratif dans Coqideherbelin
- Divers: message d'erreur et typo relatifs au langage déclaratif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-13update doc Micromegafbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11223 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-09Documentation fixes. msozeau
Thanks to Samuel Bronson for pointing out [Typeclasses unfold] was not referenced from the Setoid doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11217 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Micromega: doc + test-suite updatefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-02Improved robustness of micromega parser. Proof search of Micromega ↵fbesson
test-suites is now bounded -- ensure termination git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
Correction au passage d'un bug de Arguments Scope Global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11199 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-01correction sur la doc des modulessoubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11197 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
- Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11173 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-25Typo in documentation (isn't it?)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11172 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-25Les contraintes d'univers sont maintenant collectées dans le champs ↵soubiran
mod_constraints des modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11171 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-13Numéros de version dans la docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11123 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 00:04:46 +0000