aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24app_node, stack, state printersPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes.
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-27Abstracting away coercion indexes in Classops.Pierre-Marie Pédrot
2014-01-26Coercions: avoid imperative data structureEnrico Tassi
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment
2013-12-30When resetting an evarmap with the unsafe function Evd.evars_reset_evd withPierre-Marie Pédrot
the flag with_conv_pbs, only reset the metas, not the last_mod field. It seemed strange to mix two unrelated things. This did not break anything visible...
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
2013-12-06Fix test-suite/success/evars.v.Arnaud Spiwack
In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected).
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-11-30Better heuristic for name generation backward compatibility. We fallbackPierre-Marie Pédrot
to old behaviour whenever we were in Program mode.
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
2013-11-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
new-tacticals merge. This is essentially a revert of 6fea2f which broke the sacrosanct backward compatibility of name generation, thus breaking quite a lot of contribs.
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
parsing is plugged.
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
In 0c7a77, I inadvertantly re-defined an is_section_variable function.
2013-11-25Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
Revealed by message on coq-club on 24/11/2013.
2013-11-14Update comments in matching.mli.aspiwack
The comments were inaccurate after r16533. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-08Removing partial applications in Reductionops.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17071 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-07Partial application hunt.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17063 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Nicer infered names in refine.aspiwack
When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02push_rel_context: do not rename section variables.aspiwack
Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17024 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix compilation of pattern matching wrt variables: alias.aspiwack
Aliases (as clause) are a bit tricky. In Goal True, refine match 0 with | S n as p => _ | _ => I end Must produce the goal n:nat, p := S n : nat |- True However, in the deep branches: refine match 0 with | S (S n as p) => _ | _ => I end The alias is used to give a name to the variable of the first S : p:nat, n:nat |- True Before this patch, the goal would be p:nat, n:nat, p:=p : nat |- True Alias was used both to name the variable of the first S and to alias it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17022 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
Compilation of pattern-matching used to systematically introduce a dummy alias x:=x in the typing environment for each variable x in the patterns (except for purely variable patterns which correctly alias the term being matched). This interfered badly with the new refine implementation. To correct this I changed the "all variables" case of pattern-matching compilation to check whether the term currently being matched is a term introduced by the user or a subterm which is necessarily a variable. In the latter case, no alias is introduced. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17020 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A newly introduced variable inside a named context is no longer α-renamed.aspiwack
Instead, in case of collision, the older name is substituted for a fresh one. It should also be made inaccessible from the user, but I'll leave this for later. The goal is to guarantee that [refine (fun x => _)] introduces a binder named [x]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16972 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Efficient filtered functions in Evd. We test that a filter is actuallyppedrot
different from the identity before trying to compute filtered env/hyps. According to profiling, it seems that the filter operation is NEVER taken, that is, all filters that reach toplevel are dummy. There is surely something to do here... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16960 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-30Various optimizations of Evd.meta_* functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16958 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-30More efficient implementation of [Evd.retract_coercible_metas].ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16957 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Optimization in unification: when checking that the head of a term is anppedrot
evar or a meta, don't reconstruct the whole term. This hopefully saves a lot of useless allocations and computing time. I may have slightly changed the heuristic though, as only evars in front of applications where recognized as such, whereas now this pass through cases and fixpoints. I am walking on thin ice, but the test-suite was OK... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16956 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Useless array-to-list casts in Unification.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16955 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16953 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29[Reductionops.append_stack_app]: do not allocate a useless array.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16952 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Sharing identity evar filters.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16948 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29- install evar printer for debuggingmsozeau
- make unification try canonical structures before expansion as in evar_conv - add a fast path to evar inversion (patch from B. Ziliani). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16945 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-28Removing Evd.undefined_evars.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16942 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27Removing useless filter allocation in evar construction.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16940 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27Closure optimizations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16937 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Turn many List.assoc into List.assoc_fletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList.index is now cList.index_f, same for index0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 03:52:23 +0000