coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-10-03	Merge PR #1084: After testing it in live, writing metas using an ↵	Maxime Dénès
	?INTERNAL#42 style is ugly
2017-09-28	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot

2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
	The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-26	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès

2017-09-25	Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵	Maxime Dénès
	let-ins and non-recursively uniform parameters
2017-09-25	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵	Maxime Dénès
	4e70791).
2017-09-23	After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.	Hugo Herbelin
	Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
2017-09-23	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin

2017-09-23	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin
	The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
2017-09-22	Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵	Maxime Dénès
	context obtained by ltac pattern-matching)
2017-09-21	Proposing meta names more distinguishable from evar names than ?M42.	Hugo Herbelin
	Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
2017-09-21	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin
	The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".
2017-09-20	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias
	An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info`
2017-09-19	Merge PR #1036: Unify EConstr.t equality	Maxime Dénès

2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
	Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+\|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j \| }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
2017-09-15	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès

2017-09-15	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès

2017-09-15	Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵	Maxime Dénès
	anonymous variables)
2017-09-12	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond

2017-09-08	Using EConstr equality check in unification.	Pierre-Marie Pédrot
	The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr.
2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
	When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
	The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-08-31	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès

2017-08-31	Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate	Maxime Dénès

2017-08-31	Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag	Maxime Dénès

2017-08-31	Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵	Maxime Dénès
	implementation from Detyping.
2017-08-29	Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170	Maxime Dénès

2017-08-29	Merge PR #946: Functional pretyping interface	Maxime Dénès

2017-08-29	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin
	(from module List).
2017-08-25	primproj: fix bug 5245, hnf on proj with simpl never flag.	Matthieu Sozeau

2017-08-24	Program: fix BZ#5683, missing lift when building case predicate	Matthieu Sozeau

2017-08-22	use OCaml 4.03-compatible Filename functions	Paul Steckler

2017-08-22	Prevent overallocation in Array.map_to_list and remove custom implementation ↵	Guillaume Melquiond
	from Detyping.
2017-08-18	use OCaml temp_file, instead of our own version	Paul Steckler

2017-08-18	move filename search to start_profiler	Paul Steckler

2017-08-17	Add native compute profiling, BZ#5170	Paul Steckler

2017-08-16	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès

2017-08-01	Remove understand_tcc_evars.	Maxime Dénès
	Use the functional interface understand_tcc instead.
2017-08-01	Move type_uconstr to Tacinterp.	Maxime Dénès

2017-08-01	Remove understand_judgment and understand_judgment_tcc.	Maxime Dénès

2017-08-01	Remove allow_anonymous_refs.	Maxime Dénès

2017-08-01	Remove pure_open_constr (now open_constr)	Maxime Dénès

2017-08-01	Move glob_constr_ltac_closure to evar_refiner.	Maxime Dénès

2017-08-01	Merge PR #913: Less allocations in Detyping	Maxime Dénès

2017-08-01	Merge PR #806: closing bug 5315	Maxime Dénès

2017-07-31	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès

2017-07-29	closing bug 5315	Julien Forest

2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-26	Add a comment regarding the specialization of the combinator in Detyping.	Pierre-Marie Pédrot

2017-07-26	Removing template polymorphism for definitions.	Pierre-Marie Pédrot
	The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.