aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
| | | | | - Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only.
* Minor cleaning.Gravatar Maxime Dénès2014-07-22
|
* Revert "Extend subterm relation to pattern matching in return predicates."Gravatar Maxime Dénès2014-07-22
| | | | This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13.
* Revert "Propagate size info through pattern matching in predicates, for the"Gravatar Maxime Dénès2014-07-22
| | | | | | This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea. Apply again if this kind of dependently typed programming idioms are needed.
* Propagate size info through pattern matching in predicates, for theGravatar Maxime Dénès2014-07-22
| | | | | | | commutative cut rule. The error messages of the guard checker are now sometimes not informative enough.
* Extend subterm relation to pattern matching in return predicates.Gravatar Maxime Dénès2014-07-22
| | | | | | | | | | A pattern matching is can now be a subterm if: - Every branch is a subterm - The return predicate is a pattern matching whose return predicate is an arity. - That pattern matching (in the return predicate) returns the same inductive family in the conclusion of each branch. The commutative cut rule hasn't been updated accordingly yet.
* Fix check_inductive_codomain.Gravatar Maxime Dénès2014-07-22
|
* Refine check_is_subterm.Gravatar Maxime Dénès2014-07-22
| | | | | | | Following Bruno's suggestion, we check if the tree expected for the recursive argument is included in the one which is inferred. This check is probably not necessary in the current state of affairs, but might become so after further extensions of the guard condition.
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
| | | | extensions.
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
|
* Typo in comment.Gravatar Maxime Dénès2014-07-22
|
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
|
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
| | | | | | instantiated in the return predicate are now taken into account. The resulting recargs tree is the intersection between the one of the branches and the appearing in the return predicate. Both the domain and co-domain are filtered.
* Tentative fix for the commutative cut subterm rule.Gravatar Maxime Dénès2014-07-22
| | | | | Some fixpoints are now rejected in the standard library, but that's probably because we compare trees for equality instead of intersecting them.
* Tentative patch for incompatibility between subterm relation and dependentGravatar Maxime Dénès2014-07-22
| | | | | | | | | | | | pattern matching. This patch should be improved in two ways: (1) Implement the same checks for the commutative cut subterm rule. (2) When checking safe recursive subterms for each of the branches in a match, instanciated parameters in the return predicate should be taken into account. Step (1) should be enough to restore a correct guard condition, but (2) will be required if we don't want to rule out some legitimate and practical examples.
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
|
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
| | | | | and disable hashconsing of substituted instances which had a huge performance penalty in general. They are hashconsed when put in the environment only now.
* Cleanup code for constant equality in kernel conversion.Gravatar Matthieu Sozeau2014-07-21
|
* Use kernel conversion on terms that contain universe variables during ↵Gravatar Matthieu Sozeau2014-07-20
| | | | | | unification, speeding it up considerably Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
| | | | more than one constructor.
* Overlooked to remove a change in kernel/closure that made reducing underGravatar Matthieu Sozeau2014-07-10
| | | | a primitive projection impossible.
* Fixing the previous patch to keep transparent states in sync.Gravatar Pierre-Marie Pédrot2014-07-09
|
* Recovering transparent state from kernel oracles in constant time.Gravatar Pierre-Marie Pédrot2014-07-09
|
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in ↵Gravatar Matthieu Sozeau2014-07-07
| | | | MathClasses).
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
| | | | kernel in library/universes.ml.
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
| | | | | generated by a mutual inductive definition (bug found in CFGV). Actually this code can move out of the kernel.
* Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵Gravatar Matthieu Sozeau2014-07-03
| | | | | | cleanly when called on partially applied constructors. Also protect evar_conv from that case.
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a global reference that the current (goal) env contains all the section variables that the global reference expects to be present. Note that the test for inclusion might be costly: everytime a conversion happens in a section variable copied in a goal, this conversion has to be redone when referring to a constant dependent on this section variable. It is unclear to me whether we should not instead give global names to section variables so that they exist even if they are not listed in the context of the current goal. Here are two examples which are still problematic: Section A. Let B := True : Type. Definition C := eq_refl : B = True. Theorem D : Type. clearbody B. set (x := C). unfold C in x. (* inconsistent context *) or Section A. Let B : Type. exact True. Qed. Definition C := eq_refl : B = True. (* Note that this violated the Qed. *) Theorem D : Type. set (x := C). unfold C in x. (* inconsistent context *)
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
* Fix type_of_inductive_knowing_conclusion, relying on an actually broken ↵Gravatar Matthieu Sozeau2014-06-25
| | | | | | | univ_depends. Also add a missing constraint when generating a fresh universe for a template polymorphic inductive in that case.
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
| | | | Every time you use abstract a kitten dies, please stop.
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-21
|
* Fix computation of inductive level in monomorphism + indices-matter mode.Gravatar Matthieu Sozeau2014-06-20
| | | | Fixes bug #3346.
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
|
* Fix a destArity that does not exactly match isArity in presence of let-ins.Gravatar Matthieu Sozeau2014-06-17
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
| | | | | - Fix HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered.
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
|
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
| | | | | | | a projection constant only of the form λ params (r : I params), match r with BuildR args => args_i end, without any other user input and relies on it being typable (no more primitive projections escaping this).
* Preemptively remove files from native compilation.Gravatar Guillaume Melquiond2014-06-16
| | | | | | Ocaml does not remove the .cmi file if compilation fails, thus causing subsequent native compilations to fail due to mismatching interfaces. For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
|
* Code cleaning in Univ.Gravatar Pierre-Marie Pédrot2014-06-12
|
* In generalized rewrite, avoid retyping completely and constantly the ↵Gravatar Matthieu Sozeau2014-06-11
| | | | | | | conclusion, and results of unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x speedup in Ncring_polynom.
* Fixing Sorting Universes in a world where le and lt constraints may beGravatar Pierre-Marie Pédrot2014-06-10
| | | | redundant in canonical arcs.
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
| | | | by the printing options (i.e. when "Print Universes" is set).
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
| | | | by the printer anyway.
* Specialize the type of [Univ.compare_neq] so that it is clear it is only usedGravatar Pierre-Marie Pédrot2014-06-10
| | | | to recover the trace of a universe inconsistency. Changed its name too btw.
* Imperatively check touched universes in compare_neq functions. This ensuresGravatar Pierre-Marie Pédrot2014-06-10
| | | | | | a O(1) check, contrasting with the previous O(n) behaviour that rendered universe constraint checking prohibitive on big files. I expect a 20% speedup on such files.
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
| | | | - More cleanup. remove unneeded functions in universes
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 16:00:18 +0000