Command Index

a | b | c | d | e | f | g | i | l | m | o | p | r | s | t | u | v | ‘

	a
	Add Printing Constructor ‘ident’.
	Add Printing If ‘ident’.
	Add Printing Let ‘ident’.
	Add Printing Record ‘ident’.
	Arguments ‘qualid’ : clear implicits.
	Arguments ‘qualid’ : clear scopes
	Arguments ‘qualid’ : default implicits.
	Arguments ‘qualid’ ‘name’ : ‘rename’.
	Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’
	Arguments ‘qualid’ ‘possibly_bracketed_ident’.
	b
	Bind Scope ‘scope’ with ‘qualid’
	c
	Canonical Structure ‘ident’ : ‘type’ := ‘term’.
	Canonical Structure ‘ident’ := ‘term’ : ‘type’.
	Canonical Structure ‘ident’ := ‘term’.
	Canonical Structure ‘qualid’.
	Close Scope ‘scope’
	Coercion ‘qualid’ : ‘class’ >-> ‘class’.
	Constraint ‘ident’ ‘ord’ ‘ident’.
	d
	Declare Module ‘ident’ : ‘module_type’.
	Declare Module ‘ident’ ‘module_binding’ : ‘module_type’.
	Delimit Scope ‘scope’ with ‘ident’
	e
	End ‘ident’.
	Export ‘qualid’
	f
	Function ‘ident’ ‘binder’ : ‘type’ := ‘term’
	Function ‘ident’ ‘binder’ { measure ‘term’ ‘ident’ } : ‘type’ := ‘term’
	Function ‘ident’ ‘binder’ { struct ‘ident’ } : ‘type’ := ‘term’
	Function ‘ident’ ‘binder’ { wf ‘term’ ‘ident’ } : ‘type’ := ‘term’
	Function ‘ident’ ‘binder’ { ‘decrease_annot’ } : ‘type’ := ‘term’.
	g
	Generalizable (Variable | Variables) ‘ident’…‘ident’.
	Generalizable All Variables.
	Generalizable No Variables.
	Global Arguments ‘qualid’ : default implicits
	Global Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’
	Global Arguments ‘qualid’ ‘possibly_bracketed_ident’
	Global Close Scope ‘scope’.
	Global Generalizable.
	Global Open Scope ‘scope’.
	Global | Local Arguments ‘qualid’ ‘possibly_bracketed_ident’…‘possibly_bracketed_ident’.
	i
	Implicit Type ‘ident’ : ‘type’.
	Implicit Types ( ‘ident’…‘ident’ : ‘term’ )…( ‘ident’…‘ident’ : ‘term’ )
	Implicit Types ‘ident’…‘ident’ : ‘type’.
	Import ‘qualid’.
	Include ‘module’.
	Include ‘module’<+ …<+ ‘module’.
	Infix "‘symbol’" := ‘qualid’ (‘modifier’, …, ‘modifier’).
	l
	Local Arguments ‘qualid’ : default implicits
	Local Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’
	Local Arguments ‘qualid’ ‘possibly_bracketed_ident’.
	Local Close Scope ‘scope’.
	Local Notation ‘ident’ ‘ident’…‘ident’ := ‘term’ (only parsing).
	Local Notation ‘notation’
	Local Open Scope ‘scope’.
	Local Tactic Notation
	Local Tactic Notation (at level ‘level’) ‘prod_item’…‘prod_item’ := ‘tactic’.
	Locate Module ‘qualid’.
	Locate ‘symbol’
	m
	Module [ Import | Export ].
	Module Type ‘ident’ := ‘module_type’.
	Module Type ‘ident’ ‘module_binding’ := ‘module_type’.
	Module Type ‘ident’ ‘module_binding’ := ‘module_type’<+ …<+ ‘module_type’.
	Module Type ‘ident’ ‘module_binding’.
	Module Type ‘ident’.
	Module ‘ident’ : ‘module_type’.
	Module ‘ident’ := ‘module_expression’.
	Module ‘ident’ <: ‘module_type’<: …<: ‘module_type’.
	Module ‘ident’ ‘module_binding’ : ‘module_type’ := ‘module_expression’.
	Module ‘ident’ ‘module_binding’ : ‘module_type’.
	Module ‘ident’ ‘module_binding’ := ‘module_expression’.
	Module ‘ident’ ‘module_binding’ := ‘module_expression’<+ …<+ ‘module_expression’.
	Module ‘ident’ ‘module_binding’ <: ‘module_type’<: …<: ‘module_type’ := ‘module_expression’.
	Module ‘ident’ ‘module_binding’ <: ‘module_type’<; …<; ‘module_type’.
	Module ‘ident’ ‘module_binding’.
	Module ‘ident’.
	Monomorphic ‘definition’
	o
	Open Scope ‘scope’
	p
	Polymorphic ‘definition’
	Print Grammar constr.
	Print Grammar pattern.
	Print Grammar tactic
	Print Implicit ‘qualid’.
	Print Module Type ‘ident’.
	Print Module ‘ident’.
	Print Scope scope
	Print Scopes
	Print Sorted Universes ‘string’.
	Print Sorted Universes.
	Print Table Printing If.
	Print Table Printing Let.
	Print Visibility
	Print Visibility scope
	r
	Record ‘ident’ ‘param’ : ‘sort’ := ‘ident’ { ‘ident’ ‘binder’ : ‘term’ }.
	Remove Printing If ‘ident’.
	Remove Printing Let ‘ident’.
	s
	Section ‘ident’.
	Set Contextual Implicit.
	Set Implicit Arguments.
	Set Maximal Implicit Insertion.
	Set Parsing Explicit.
	Set Printing All.
	Set Printing Existential Instances.
	Set Printing Implicit Defensive.
	Set Printing Implicit.
	Set Printing Matching.
	Set Printing Projections.
	Set Printing Synth.
	Set Printing Universes.
	Set Printing Wildcard.
	Set Reversible Pattern Implicit.
	Set Strongly Strict Implicit.
	t
	Test Printing If for ‘ident’.
	Test Printing Let for ‘ident’.
	Test Printing Matching.
	Test Printing Synth.
	Test Printing Wildcard.
	u
	Undelimit Scope ‘scope’
	Universe ‘ident’.
	Unset Maximal Implicit Insertion.
	Unset Parsing Explicit.
	Unset Printing All.
	Unset Printing Existential Instances.
	Unset Printing Implicit Defensive.
	Unset Printing Implicit.
	Unset Printing Matching.
	Unset Printing Records.
	Unset Printing Synth.
	Unset Printing Universes.
	Unset Printing Wildcard.
	Unset Strict Implicit.
	v
	Variant ‘ident’ ‘params’ : ‘sort’ := ‘ident’ (‘ident’ : ‘term_1’).
	‘
	‘assumption_keyword’ Inline ‘assums’.