aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
...
| * | Exporting ValTMap for use in Genintern.Gravatar Hugo Herbelin2017-11-02
| | |
| | * Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| |/ | | | | | | 4.02.3 has been the minimal OCaml version for a while now.
* / Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
|/ | | | This fixes also #5731, #6035, #5364.
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
* \ Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Gravatar Maxime Dénès2017-10-06
|\ \ | | | | | | | | | "_something")
* \ \ Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ | | | | | | | | | | | | BZ#5757)
* \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ | | | | | | | | | | | | | | | cleared context.
| | | * | Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | |
| | | | * Remove TODO comment (Evar.t is opaque)Gravatar Gaëtan Gilbert2017-09-29
| | | |/
* | | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
| | | |
* | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| |_|/ |/| | | | | | | | | | | 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).
| | * Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
| | * Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
| |/ |/| | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
| * Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
|/ | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* \ Merge PR #1036: Unify EConstr.t equalityGravatar Maxime Dénès2017-09-19
|\ \
| | * Document UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | |
| | * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
| | * proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | | | | | | | | | | | evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular.
| | * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |
| * Normalizing universes before performing term comparison.Gravatar Pierre-Marie Pédrot2017-09-08
| | | | | | | | | | | | This code was probably slightly wrong w.r.t. to a semantics defined as equivalent to first full-blown normalization followed by kernel term equality. Or at least, it was adding redundant constraints.
| * Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
|/ | | | | | | 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.
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #913: Less allocations in DetypingGravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \
| * | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | |
* | | | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * / No useless reallocation in Termops.collapse_appl.Gravatar Pierre-Marie Pédrot2017-07-21
|/ / | | | | | | | | | | This function is suspicious, and reallocates a lot when it should be the identity. This matters for detyping, where it is about the only place where it is used.
* | [proofs] Remove circular dependency from Proofview to Goal.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |
* | Merge PR #781: Remove dead code [Universes.simplify_universe_context]Gravatar Maxime Dénès2017-07-17
|\ \
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelGravatar Maxime Dénès2017-07-13
|\ \ \
| * | | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
| * | | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
* | | | Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵Gravatar Maxime Dénès2017-07-07
|\ \ \ \ | |/ / / |/| | | | | | | the monad.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \ \
* | | | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | | | |
| | | | * Adding intermediate entry point to create an evar in empty rel_context.Gravatar Hugo Herbelin2017-06-25
| |_|_|/ |/| | |
| | * | In enter_one, not having exactly one goal is a fatal error of the monad.Gravatar Hugo Herbelin2017-06-23
| |/ / |/| | | | | | | | Pointed out by PMP.
| | * Remove dead code [Universes.simplify_universe_context]Gravatar Gaëtan Gilbert2017-06-20
| |/ |/| | | | | Dead since 23f4804b50307766219392229757e75da9aa41d9
* | Merge PR#793: Fixing restriction of existential variables regarding evar_storeGravatar Maxime Dénès2017-06-20
|\ \
* | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| | |
* | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* | | Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
| | |
* | | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
* | | New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
| | |
| | * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| | |\
| | * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | |\ \
| * | | | Fixing restrict regarding evar_store.Gravatar Hugo Herbelin2017-06-14
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 12:29:53 +0000