aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_obligations.mli
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Add the ability to give a specific tactic to solve each obligation inmsozeau
Program. No syntax to do it yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
overriding the default tactic when adding a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 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-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Fix some bugs, add possibility of automatically solving a proof statement's ↵msozeau
obligations and start the proof afterwards. Changes the architecture of subtac_obligations a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10257 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Fix bug when adding progs with no obligationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9978 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-02Better handling of aliases, add command to solve a particular obligation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9929 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Add Solve All Obligations command, fix bug in inequality generation ↵msozeau
introduced by previous commit, add general purpose tactics for destructing existentials and disjunctions. Compiles without camlp4 warnings too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9888 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17Correct implementation of undo in obligations handling code, correct some ↵msozeau
bugs in pattern-matching compilation with multiple matched objects. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9783 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-13Solve obligation handling bug of trying to solve automatically at Next ↵msozeau
Obligation time. Now done at Qed or Defined. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9700 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Opacity parameterization for obligations working.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9675 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when ↵msozeau
needed, handle undo for the default tactic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9608 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-15Various subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-29Fork of cases impl for subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-15Some usability enhancements.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9376 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on mutual defs, various bug fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9360 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-09Support for mutual defs in obligation handling.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9357 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Work on obligation separation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9326 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Facilities to automatically solve obligationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9284 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:41:15 +0000