aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
* \ Merge PR #1084: After testing it in live, writing metas using an ↵Gravatar Maxime Dénès2017-10-03
|\ \ | | | | | | | | | ?INTERNAL#42 style is ugly
| | * Remove some duplication between Typeops and Nativenorm.Gravatar Gaëtan Gilbert2017-09-29
| | |
| | * Remove trivial TODO comment (constants can't be template poly now).Gravatar Gaëtan Gilbert2017-09-28
| | |
* | | 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).
* | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \
* \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ | | | | | | | | | | | | let-ins and non-recursively uniform parameters
* \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ | | | | | | | | | | | | | | | 4e70791).
| | | | * After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Gravatar Hugo Herbelin2017-09-23
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| * | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | |
| | * | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |/ / |/| | | | | | | | | | | | | | | | | 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".
* | | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ | | | | | | | | | | | | context obtained by ltac pattern-matching)
| * | | Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
| * | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| |/ / | | | | | | | | | | | | 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".
* | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`
* | | Merge PR #1036: Unify EConstr.t equalityGravatar Maxime Dénès2017-09-19
|\ \ \ | |/ / |/| |
| | * 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.
* | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ | | | | | | | | | | | | | | | anonymous variables)
| | | * | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|/ / |/| | |
| | | * 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.
| | * Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ |/| | | | | | | 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.
* | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \
* \ \ Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateGravatar Maxime Dénès2017-08-31
|\ \ \
* \ \ \ Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagGravatar Maxime Dénès2017-08-31
|\ \ \ \
* \ \ \ \ Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵Gravatar Maxime Dénès2017-08-31
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | implementation from Detyping.
* \ \ \ \ \ Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \
| | | | | | * | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | (from module List).
| | | | * | | primproj: fix bug 5245, hnf on proj with simpl never flag.Gravatar Matthieu Sozeau2017-08-25
| |_|_|/ / / |/| | | | |
| | | | * | Program: fix BZ#5683, missing lift when building case predicateGravatar Matthieu Sozeau2017-08-24
| |_|_|/ / |/| | | |
| | * | | use OCaml 4.03-compatible Filename functionsGravatar Paul Steckler2017-08-22
| | | | |
| | | * | Prevent overallocation in Array.map_to_list and remove custom implementation ↵Gravatar Guillaume Melquiond2017-08-22
| |_|/ / |/| | | | | | | | | | | from Detyping.
| | * | use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
| | | |
| | * | move filename search to start_profilerGravatar Paul Steckler2017-08-18
| | | |
| | * | Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| |/ / |/| |
* | | Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \
| | * | Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | | | Use the functional interface understand_tcc instead.
| | * | Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
| | | |
| | * | Remove understand_judgment and understand_judgment_tcc.Gravatar Maxime Dénès2017-08-01
| | | |
| | * | Remove allow_anonymous_refs.Gravatar Maxime Dénès2017-08-01
| | | |
| | * | Remove pure_open_constr (now open_constr)Gravatar Maxime Dénès2017-08-01
| | | |
| | * | Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
| |/ / |/| |
* | | Merge PR #913: Less allocations in DetypingGravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #806: closing bug 5315Gravatar 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
|\ \ \ \ \
| | * | | | closing bug 5315Gravatar Julien Forest2017-07-29
| |/ / / / |/| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 09:38:13 +0000