aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
...
* 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
* Oops, one refactoring was not compiled.Gravatar Matthieu Sozeau2014-06-10
|
* More cleanup/reorganizing of univ.ml to separate constraint/universe ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | handling from the instance/contexts and substitution code.
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | | | Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
* Remove unused function in univGravatar Matthieu Sozeau2014-06-10
|
* Flattening Level module structure in Univ.Gravatar Pierre-Marie Pédrot2014-06-09
|
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
| | | | | | | | | | | | | | | | | | | | | | | | declare takes care of ignoring side effects that are available in the global environment. This is yet another instance of what the "abominion" (aka abstract) can do: the code was checking for the existence in the environment of the elimination principle, and not regenerating it (nor declaring the corresponding side effect) if the elimination principle is used twice. Of course to functionalize the imperative actions on the environment when two proofs generated by abstract use the same elim principle, such elim principle has to be inlined twice, once in each abstracted proof. In other words, a side effect generated by a tactic inside an abstract is *global* but will be made local, si it must always be declared, no matter what. Now the system works like this: - side effects are always declared, even if a caching mechanism thinks the constant is already there (it can be there, no need to regenerate it but the intent to generate it *must* be declared anyhow) - at Qed time, we filter the list of side effects and decide which ones are really needed to be inlined. bottom line: STOP using abstract.
* Function in Univ uselessly exported.Gravatar Pierre-Marie Pédrot2014-06-08
|
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
| | | | | | | | | | | allowing fast conversion to be used during unification while respecting the semantics of unification w.r.t universes. - Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv is used for module subtyping. - Outside, infer_conv is wrapped in Reductionops to register the right constraints in an evarmap. - In univ, add a flag to universes to cache the fact that they are >= Set, the most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
* Dedicated map module for type universes. It uses hashmaps, which areGravatar Pierre-Marie Pédrot2014-06-05
| | | | slightly more efficient than plain balanced maps.
* Removing dead code from Univ.Gravatar Pierre-Marie Pédrot2014-06-05
|
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
| | | | - Finish the change to level-to-level substitutions, in the checker.
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
| | | | | | | - Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level substitutions where the more general level-to-universe substitutions were previously used.
* Fixing incorrect printf format.Gravatar Pierre-Marie Pédrot2014-06-02
|
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
| | | | | | cases of Type (* Prop *) <= Set. - Do check types of metavariables at the end of apply's unification, if it failed at the beginning (otherwise universe constraints can be incomplete).
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
| | | | | | | | | correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:14:45 +0000