aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/merge.ml
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-09More factorization of inductive/record and typeclasses: move classmsozeau
declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-18Added a function to rebuild an elim scheme from elim_scheme_info. Willcourtieu
use it for elim principle type generation from merged graphs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10693 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-14Backtrack wrong commit.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10667 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-13trying fcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10659 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-10-30Cleaning code and comment.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10272 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Functional graph merging deals with letins.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9404 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Fixed the graph merging parameter order.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9403 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9401 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Changing merging functional scheme syntax.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9395 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Small fix in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9383 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Fixes in experimental merging of functional graphs.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9305 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: put functional results at the endcourtieu
of args. Still a bug with parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9300 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: removed debug printing.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9296 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: names of constructors.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9295 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Some fixes in experimental merging of two functional graphs. courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9287 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Experimental merging of two functional graphs.courtieu
temporary synatx: Mergeschemes (G1 a b c) with (G2 a d e) using G1G2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9285 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Starting to add a function schemes merging command (not finished, notcourtieu
activated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9251 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 05:12:01 +0000