Files

 master

/

pretyping

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

coqbot-app[bot]

and

ppedrot

Merge PR coq#17714: Stop returning Sorts.family from Inductiveops.get…

Jun 13, 2023

ca8db7b · Jun 13, 2023

History

History

This branch is 4702 commits behind coq/coq:master.

/

pretyping

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
arguments_renaming.ml		arguments_renaming.ml	Sharing check_hyps_inclusion with evars between retyping and typing	Mar 31, 2023
arguments_renaming.mli		arguments_renaming.mli	Sharing check_hyps_inclusion with evars between retyping and typing	Mar 31, 2023
cases.ml		cases.ml	Stop returning Sorts.family from Inductiveops.get_arity	Jun 9, 2023
cases.mli		cases.mli	Fixing coq#14207: multiple warning unused variable catching several c…	May 6, 2021
cbv.ml		cbv.ml	Use UnsafeMonomorphic for primitive types in cbv and reductionops	Mar 6, 2023
cbv.mli		cbv.mli	Use lists instead of arrays for cbv application nodes.	Apr 10, 2022
coercion.ml		coercion.ml	Cleanup declare_X_option_and_ref APIs	Jun 5, 2023
coercion.mli		coercion.mli	Add a use_coercions flag to pretype_flags	Apr 15, 2022
coercionops.ml		coercionops.ml	Remove low-value warning categories	May 26, 2023
coercionops.mli		coercionops.mli	[elaborator] reversible coercions	Apr 28, 2022
constr_matching.ml		constr_matching.ml	Revised warning API: warnings can have multiple categories	May 26, 2023
constr_matching.mli		constr_matching.mli	Abstract away the type of matching contexts.	May 9, 2022
detyping.ml		detyping.ml	Use Deprecation.t for deprecated goptions	Jun 5, 2023
detyping.mli		detyping.mli	Remove detyping lax argument	Jan 16, 2023
dune		dune	Enable warning 70 (missing mli), add mli files	Apr 17, 2023
evarconv.ml		evarconv.ml	Rename decompose_app->decompose_app_list, decompose_app_vect->decompo…	May 24, 2023
evarconv.mli		evarconv.mli	Simplify Evarconv.occurence_match_test	Oct 20, 2022
evardefine.ml		evardefine.ml	Fix relevance of domain in define_pure_evar_as_product.	Feb 8, 2023
evardefine.mli		evardefine.mli	Preserve the ESorts abstraction in the upper layers.	Dec 5, 2022
evarsolve.ml		evarsolve.ml	Rename decompose_app->decompose_app_list, decompose_app_vect->decompo…	May 24, 2023
evarsolve.mli		evarsolve.mli	Remove unification flag "allow_K_at_toplevel"	Oct 20, 2022
find_subterm.ml		find_subterm.ml	Fix catching univ inconsistencies in Find_subterm.make_eq_univs_test	Aug 12, 2022
find_subterm.mli		find_subterm.mli	Change the representation of kernel case.	Jan 4, 2021
genarg.ml		genarg.ml	Add genarg dumping APIs	Mar 29, 2023
genarg.mli		genarg.mli	Add genarg dumping APIs	Mar 29, 2023
geninterp.ml		geninterp.ml	Update headers in the whole code base.	Mar 18, 2020
geninterp.mli		geninterp.mli	Update headers in the whole code base.	Mar 18, 2020
globEnv.ml		globEnv.ml	More robust reinterpreting of ltac variables	May 5, 2023
globEnv.mli		globEnv.mli	Move the responsibility of type-checking to the caller for tactic-in-…	Mar 12, 2021
glob_ops.ml		glob_ops.ml	Revised warning API: warnings can have multiple categories	May 26, 2023
glob_ops.mli		glob_ops.mli	Remove REVERTcast	Oct 4, 2021
glob_term.mli		glob_term.mli	Enable warning 70 (missing mli), add mli files	Apr 17, 2023
heads.ml		heads.ml	Port Heads to EConstr.	Sep 5, 2022
heads.mli		heads.mli	Port Heads to EConstr.	Sep 5, 2022
indrec.ml		indrec.ml	Stop returning Sorts.family from Inductiveops.get_arity	Jun 9, 2023
indrec.mli		indrec.mli	Move back the case-building function for case_pf to Clenv.	Apr 24, 2023
inductiveops.ml		inductiveops.ml	Stop returning Sorts.family from Inductiveops.get_arity	Jun 9, 2023
inductiveops.mli		inductiveops.mli	Stop returning Sorts.family from Inductiveops.get_arity	Jun 9, 2023
keys.ml		keys.ml	Leaf objects do not need a low level id	Dec 9, 2021
keys.mli		keys.mli	Update headers in the whole code base.	Mar 18, 2020
locus.mli		locus.mli	Enable warning 70 (missing mli), add mli files	Apr 17, 2023
locusops.ml		locusops.ml	Add checks for invalid occurrences in setoid rewrite.	Dec 14, 2020
locusops.mli		locusops.mli	Add checks for invalid occurrences in setoid rewrite.	Dec 14, 2020
ltac_pretype.mli		ltac_pretype.mli	Enable warning 70 (missing mli), add mli files	Apr 17, 2023
nativenorm.ml		nativenorm.ml	Cleanup declare_X_option_and_ref APIs	Jun 5, 2023
nativenorm.mli		nativenorm.mli	Move {native,vm}_infer_conv definitions to reductionops	Dec 7, 2021
pattern.mli		pattern.mli	Enable warning 70 (missing mli), add mli files	Apr 17, 2023
patternops.ml		patternops.ml	Revised warning API: warnings can have multiple categories	May 26, 2023
patternops.mli		patternops.mli	Use a set instead of a list in pattern internalization.	Mar 17, 2023
pretype_errors.ml		pretype_errors.ml	Typing: don't forget unification error for CantApplyBadType	Jun 8, 2023
pretype_errors.mli		pretype_errors.mli	Typing: don't forget unification error for CantApplyBadType	Jun 8, 2023
pretyping.ml		pretyping.ml	Stop returning Sorts.family from Inductiveops.get_arity	Jun 9, 2023
pretyping.mli		pretyping.mli	Ltac2 preterm antiquotation $preterm:x	Jun 8, 2023
program.ml		program.ml	Use Deprecation.t for deprecated goptions	Jun 5, 2023
program.mli		program.mli	Remove calls to the Global module from pretyping/program and percolate.	Dec 31, 2021
reductionops.ml		reductionops.ml	Rename decompose_app->decompose_app_list, decompose_app_vect->decompo…	May 24, 2023
reductionops.mli		reductionops.mli	Kernel: split reduction.ml to have conversion-related functions in co…	Apr 27, 2023
retyping.ml		retyping.ml	Merge PR coq#17633: Move Termops.decompose_app_vect to EConstr, renam…	May 30, 2023
retyping.mli		retyping.mli	nf_relevance: also handle variables set above_prop	May 23, 2023
structures.ml		structures.ml	Merge PR coq#17585: Revised warning API: warnings can have multiple c…	May 30, 2023
structures.mli		structures.mli	Correct comment in structures.mli	Dec 16, 2022
tacred.ml		tacred.ml	Rename decompose_app->decompose_app_list, decompose_app_vect->decompo…	May 24, 2023
tacred.mli		tacred.mli	Use custom exception for "cannot coerce to an evaluable reference"	Jan 27, 2023
typeclasses.ml		typeclasses.ml	Cleanup declare_X_option_and_ref APIs	Jun 5, 2023
typeclasses.mli		typeclasses.mli	Use a set instead of a list in pattern internalization.	Mar 17, 2023
typeclasses_errors.ml		typeclasses_errors.ml	Update headers in the whole code base.	Mar 18, 2020
typeclasses_errors.mli		typeclasses_errors.mli	Update headers in the whole code base.	Mar 18, 2020
typing.ml		typing.ml	Typing: don't forget unification error for CantApplyBadType	Jun 8, 2023
typing.mli		typing.mli	Use new warning API to provide nicer printer for bad relevance warning	May 26, 2023
unification.ml		unification.ml	Cleanup declare_X_option_and_ref APIs	Jun 5, 2023
unification.mli		unification.mli	Avoid Evd.empty in destruct/induction	Apr 3, 2023
vnorm.ml		vnorm.ml	Rename decompose_app->decompose_app_list, decompose_app_vect->decompo…	May 24, 2023
vnorm.mli		vnorm.mli	Update headers in the whole code base.	Mar 18, 2020
View all files