aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Maxime Dénès
alphabet
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
To this extent we factor out the relevant bits to a new file, ltac_pretype.
2017-10-17unification: fix BZ#5692, recognize prim projs as CS projectionsMatthieu Sozeau
2017-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-10-17Handling primitive projections in canonical structures.Pierre-Marie Pédrot
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ↵Maxime Dénès
?INTERNAL#42 style is ugly
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
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).
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Maxime Dénès
let-ins and non-recursively uniform parameters
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Maxime Dénès
4e70791).
2017-09-23After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Hugo Herbelin
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).
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
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".
2017-09-22Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵Maxime Dénès
context obtained by ltac pattern-matching)
2017-09-21Proposing meta names more distinguishable from evar names than ?M42.Hugo Herbelin
Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
2017-09-21A possible fix to BZ#5750 (ability to print context of ltac subterm match).Hugo Herbelin
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".
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
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`
2017-09-19Merge PR #1036: Unify EConstr.t equalityMaxime Dénès
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
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.
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Maxime Dénès
anonymous variables)
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-08Using EConstr equality check in unification.Pierre-Marie Pédrot
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.
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
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.
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
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.
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-31Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateMaxime Dénès
2017-08-31Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagMaxime Dénès
2017-08-31Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵Maxime Dénès
implementation from Detyping.
2017-08-29Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Maxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
(from module List).
2017-08-25primproj: fix bug 5245, hnf on proj with simpl never flag.Matthieu Sozeau
2017-08-24Program: fix BZ#5683, missing lift when building case predicateMatthieu Sozeau
2017-08-22use OCaml 4.03-compatible Filename functionsPaul Steckler
2017-08-22Prevent overallocation in Array.map_to_list and remove custom implementation ↵Guillaume Melquiond
from Detyping.
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-18move filename search to start_profilerPaul Steckler
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-01Remove understand_tcc_evars.Maxime Dénès
Use the functional interface understand_tcc instead.
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-08-01Remove understand_judgment and understand_judgment_tcc.Maxime Dénès
2017-08-01Remove allow_anonymous_refs.Maxime Dénès
2017-08-01Remove pure_open_constr (now open_constr)Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 05:42:39 +0000