diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:32 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:32 +0000 |
| commit | a92a276d9aadf321262e5b767a809642708c5cc5 (patch) | |
| tree | bcfdf7e0e94481ff9a171056baf749c277b18dbb /pretyping/cases.mli | |
| parent | 8ead702b4f0ec5e0fecfc5de68f7ce86f56b20fe (diff) | |
Fix the compilation of pattern matching wrt to variables.
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
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 3e4b09148..ca3c77aad 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -86,8 +86,12 @@ type tomatch_type = | IsInd of types * inductive_type * Name.t list | NotInd of constr option * types +(* spiwack: The first argument of [Pushed] is [true] for initial + Pushed and [false] otherwise. Used to decide whether the term being + matched on must be aliased in the variable case (only initial + Pushed need to be aliased). *) type tomatch_status = - | Pushed of ((constr * tomatch_type) * int list * Name.t) + | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (Name.t * constr * (constr * types)) | NonDepAlias | Abstract of int * rel_declaration |