matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 5 Sep 2015 15:14:26 +0000 (15:14 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 5 Sep 2015 15:14:26 +0000 (15:14 +0000)
commit	6c15dd2d7c372dc163c24e96bf56376c5bcb5a6c
tree	ce5b9bd355cfbf2653974bd6864b7d21cc165afb	tree \| snapshot
parent	c1175e54bf8d17e41c1f0789ec2bad57aedb9b8c	commit \| diff

- New attribute `Implied put beside `Generated and `Provided.
  It denotes an object provided not as defined by the user, but as generated by another ITP
  New optional keyword "implied" recognized in front of:
  theorem, definition, ..., let rec, let corec
  specifies to construct an object with this new attribute.
  [still not admitted in front of inductive, coinductive, record]

29 files changed:

matita/components/binaries/probe/options.mli		diff \| blob \| history
matita/components/binaries/probe/probe.ml		diff \| blob \| history
matita/components/content/.depend		diff \| blob \| history
matita/components/content_pres/.depend		diff \| blob \| history
matita/components/disambiguation/.depend		diff \| blob \| history
matita/components/extlib/.depend		diff \| blob \| history
matita/components/getter/.depend		diff \| blob \| history
matita/components/grafite/.depend		diff \| blob \| history
matita/components/grafite_engine/.depend		diff \| blob \| history
matita/components/grafite_parser/.depend		diff \| blob \| history
matita/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
matita/components/library/.depend		diff \| blob \| history
matita/components/logger/.depend		diff \| blob \| history
matita/components/ng_cic_content/.depend		diff \| blob \| history
matita/components/ng_disambiguation/.depend		diff \| blob \| history
matita/components/ng_extraction/.depend	[new file with mode: 0644]	blob
matita/components/ng_kernel/.depend		diff \| blob \| history
matita/components/ng_kernel/nCic.ml		diff \| blob \| history
matita/components/ng_kernel/nCicPp.ml		diff \| blob \| history
matita/components/ng_library/.depend		diff \| blob \| history
matita/components/ng_paramodulation/.depend		diff \| blob \| history
matita/components/ng_refiner/.depend		diff \| blob \| history
matita/components/ng_tactics/.depend		diff \| blob \| history
matita/components/registry/.depend		diff \| blob \| history
matita/components/thread/.depend		diff \| blob \| history
matita/components/xml/.depend		diff \| blob \| history
matita/matita/.depend		diff \| blob \| history
matita/matita/.depend.opt		diff \| blob \| history
matita/matita/matita.lang		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom