aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/g_subtac.ml4
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-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-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-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-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Use new redefinition support for the default obligations tacticmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10485 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ↵msozeau
wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 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-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 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-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-02-02Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterherbelin
de cacher l'instance de la règle figurant dans g_constr (report révision 9588 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9589 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-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des wit_tactic en types créés dynamiquement (révisions 8917 et 8926). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 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-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-09-01New handling of obligations.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9120 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Subtac fixes, new way of handling obligations in progress.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9117 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-07- Documentation of the Program tactics.msozeau
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 00:04:29 +0000