coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Renaming new_induct -> induction; new_destruct -> destruct.	Hugo Herbelin	2014-05-08
\|
*	Little reorganization of generalize tactics code w/o semantic changes.	Hugo Herbelin	2014-05-08
\| \| \| \|	Also removing trailing spaces.
*	Cleanup code in pretyping/evarutil	Matthieu Sozeau	2014-05-08
\|
*	Fix performance problem with unification in presence of universes (bug ↵	Matthieu Sozeau	2014-05-08
\| \| \| \| \| \| \|	#3302) by considering Type i a ground term even when "i" is a flexible universe variable, using the infer_conv function to do the unification of universes.
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵	Matthieu Sozeau	2014-05-08
\| \| \| \| \| \| \| \|	evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet).
*	Avoid allocations in type_of_inductive	Matthieu Sozeau	2014-05-08
\|
*	Fast-path equality of sorts in compare_constr*	Matthieu Sozeau	2014-05-08
\|
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
\|
*	Moving Dnet-related code to tactics/.	Pierre-Marie Pédrot	2014-05-08
\|
*	Fixing test-suite for bug #3043.	Pierre-Marie Pédrot	2014-05-08
\|
*	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot	2014-05-08
\| \| \| \|	shows the polymorphism status of the term.
*	Code cleaning in Tacinterp: factorizing some uses of tclEVARS.	Pierre-Marie Pédrot	2014-05-08
\|
*	Removing comment outdated since eta holds in conversion rule (this	Hugo Herbelin	2014-05-07
\| \| \| \|	answers #3299).
*	Adding test-suite for bug #3242.	Pierre-Marie Pédrot	2014-05-06
\|
*	Remove Lemmas from base_include, it's not linked in dev/printers anymore	Matthieu Sozeau	2014-05-06
\|
*	Cleanup before merge with the trunk	Matthieu Sozeau	2014-05-06
\|
*	Use new tactic combinators in tclABSTRACT, to avoid blowup when using ↵	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \|	V82.tactic (tclEVARS _). Again, performance is back to normal. Remove reintroduced try .. with _ -> in raw_enter's.
*	Add missing case for primitive projection in fold_map.	Matthieu Sozeau	2014-05-06
\|
*	Fix after merge.	Matthieu Sozeau	2014-05-06
\|
*	Add incompatibilities paragraph in doc about universe polymorphism.	Matthieu Sozeau	2014-05-06
\|
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \| \| \| \|	in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. - Fix a HUGE performance problem in the processing of constraints, which was remerging all the previous constraints with the ambient global universes at each new constraint addition. Performance is now back to (or better than) normal.
*	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau	2014-05-06
\| \| \| \| \|	Fix restriction of universe contexts to not forget about potentially useful constraints.
*	Fix Field_tac to get fast reification again, with the fix on template ↵	Matthieu Sozeau	2014-05-06
\| \| \| \|	universe polymorphic constructors.
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \| \|	eagerly solve l <= k constraints as k := l when k is a fresh variable coming from a template type. This has the effect of fixing the variable at the first instantiation of the parameters of template polymorphic inductive and avoiding to generate useless <= constraints that need to be minimized afterwards.
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
\|
*	Print universes in module printing	Matthieu Sozeau	2014-05-06
\|
*	Fix funind w.r.t. universes	Matthieu Sozeau	2014-05-06
\|
*	Fix a pervasive equality use.	Matthieu Sozeau	2014-05-06
\|
*	Avoid u+k <= v constraints, don't take the sup of an algebraic universe during	Matthieu Sozeau	2014-05-06
\| \| \| \|	minimization.
*	- Add back some compatibility functions to avoid rewriting plugins.	Matthieu Sozeau	2014-05-06
\| \| \| \| \|	- Fix in canonical structure inferce, we have to check that the heads are convertible and keep universe information around.
*	Add doc on the new API for universe polymorphism and primitive projections	Matthieu Sozeau	2014-05-06
\|
*	Fix derive plugin to properly treat universes	Matthieu Sozeau	2014-05-06
\|
*	Keep track of universes on coercion applications even if they're not ↵	Matthieu Sozeau	2014-05-06
\| \| \| \|	polymorphic (fixes bug #3043).
*	Comment in Funind.v test-suite file	Matthieu Sozeau	2014-05-06
\|
*	Proper calculation of constructor levels, forgetting the level of lets.	Matthieu Sozeau	2014-05-06
\|
*	Refresh some universes in cases.ml as they might appear in the term.	Matthieu Sozeau	2014-05-06
\|
*	Correct universe handling in program coercions (bug #2378).	Matthieu Sozeau	2014-05-06
\|
*	Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.	Matthieu Sozeau	2014-05-06
\|
*	Retype application of fix_proto to get the right universes in Program	Matthieu Sozeau	2014-05-06
\|
*	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \|	- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints. (Needs to be enforced in the kernel as well, but that's the main entry point). - Fix a test-suite script and remove a regression comment, it's just as before now.
*	Fix restrict_universe_context removing some universes that do appear in the ↵	Matthieu Sozeau	2014-05-06
\| \| \| \|	term.
*	Fix declarations of monomorphic assumptions	Matthieu Sozeau	2014-05-06
\|
*	Allow records whose sort is defined by a constant.	Matthieu Sozeau	2014-05-06
\|
*	- Fix RecTutorial, and mutual induction schemes getting the wrong names.	Matthieu Sozeau	2014-05-06
\| \| \| \|	Now the universe inconsistency appears at [exact t] instead of the Defined :)
*	Fix program Fixpoint not taking care of universes.	Matthieu Sozeau	2014-05-06
\|
*	- Fixes for canonical structure resolution (check that the initial term ↵	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \| \| \|	indeed unifies with the projected term, keeping track of universes). - Fix the [unify] tactic to fail properly. - Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
*	Fix restrict_universe_context to not remove useful constraints.	Matthieu Sozeau	2014-05-06
\|
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \|	- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even in presence of polymorphism - Correctly mark unresolvable the evars made by the Simple abstraction.
*	Remove postponed constraints (unused)	Matthieu Sozeau	2014-05-06
\|
*	Fixes after rebase. The use of pf_constr_of_global is problematic in ↵	Matthieu Sozeau	2014-05-06
\| \| \| \|	presence of side-effects...