aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
| | | | | | | There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
| | | | | NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
|
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Removing a Pervasives.compare in Term_dnet.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an ↵Gravatar Pierre Boutillier2014-02-28
| | | | infinite loop.
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
|
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
| | | Adds a combinator List.map_right which chains effects from right to left.
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
|
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
| | | | | When you resume the compilation of a .vi file, you want to avoid collisions on fresh names.
* IStream: change type of thunk, spare allocations.Gravatar Arnaud Spiwack2014-02-24
| | | | | | | Two changes: - 'a Lazy.t becomes unit -> 'a - 'a t becomes 'a u (the view type) This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.
* Ensuring that the module Stack is opaque inside Reductionops.Gravatar Pierre-Marie Pédrot2014-02-24
|
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
| | | | (excepts list of args that must be constructors
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
| | | | syntax mentionning simpl remains
* Create Debug Unification optionGravatar Pierre Boutillier2014-02-24
| | | | to dump states that Evarconv.eq_appr_x tries to unify.
* No more translation array <-> list in Reductionops.StackGravatar Pierre Boutillier2014-02-24
|
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
|
* Reductionops.Stack.app_node is secretGravatar Pierre Boutillier2014-02-24
|
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
|
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
|
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
| | | | | | The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes.
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
|
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Using Map.smartmap whenever deemed useful.Gravatar Pierre-Marie Pédrot2014-01-29
|
* Abstracting away coercion indexes in Classops.Gravatar Pierre-Marie Pédrot2014-01-27
|
* Coercions: avoid imperative data structureGravatar Enrico Tassi2014-01-26
|
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
| | | | | | | Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment
* When resetting an evarmap with the unsafe function Evd.evars_reset_evd withGravatar Pierre-Marie Pédrot2013-12-30
| | | | | 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...
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
| | | | | | | | | | | | | | | | 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.
* Fix test-suite/success/evars.v.Gravatar Arnaud Spiwack2013-12-06
| | | 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).
* Removing useless meta-related functions.Gravatar Pierre-Marie Pédrot2013-12-03
|
* Better heuristic for name generation backward compatibility. We fallbackGravatar Pierre-Marie Pédrot2013-11-30
| | | | to old behaviour whenever we were in Program mode.
* Useless instantiation function exported in Evd.Gravatar Pierre-Marie Pédrot2013-11-30
|
* Tentative fix to recover fresh name generation as it was beforeGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | 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.
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Factoring: is_section_variable.Gravatar Arnaud Spiwack2013-11-25
| | | | In 0c7a77, I inadvertantly re-defined an is_section_variable function.
* Typo resulting in bad eta-expansion of destructing let's body.Gravatar Hugo Herbelin2013-11-25
| | | | Revealed by message on coq-club on 24/11/2013.
* Update comments in matching.mli.Gravatar aspiwack2013-11-14
| | | | | | The comments were inaccurate after r16533. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing partial applications in Reductionops.Gravatar ppedrot2013-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial application hunt.Gravatar ppedrot2013-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preventing useless allocations in Reductionops.instance.Gravatar ppedrot2013-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
| | | | | | 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
* push_rel_context: do not rename section variables.Gravatar aspiwack2013-11-02
| | | | | | 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
* Fix compilation of pattern matching wrt variables: alias.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fix the compilation of pattern matching wrt to variables.Gravatar aspiwack2013-11-02
| | | | | | | | 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
* A newly introduced variable inside a named context is no longer α-renamed.Gravatar aspiwack2013-11-02
| | | | | | | | | 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
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
| | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 20:38:35 +0000