diff options
author | 2014-09-30 09:13:40 +0200 | |
---|---|---|
committer | 2014-09-30 09:30:53 +0200 | |
commit | 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f (patch) | |
tree | 53478ded9dfb8108402d7f45fa1300edd1569a20 /pretyping/glob_ops.ml | |
parent | 2bbf1305a080667d8547c44b2684010aba3d8d45 (diff) |
Add syntax for naming new goals in refine: writing ?[id] instead of _
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
Diffstat (limited to 'pretyping/glob_ops.ml')
-rw-r--r-- | pretyping/glob_ops.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9157cdb81..fd51545b2 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -96,8 +96,9 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with Array.equal glob_constr_eq c1 c2 && Array.equal glob_constr_eq t1 t2 | GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2 -| GHole (_, kn1, gn1), GHole (_, kn2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) +| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (_, c1, t1), GCast (_, c2, t2) -> glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 | _ -> false @@ -342,7 +343,7 @@ let loc_of_glob_constr = function | GIf (loc,_,_,_,_) -> loc | GRec (loc,_,_,_,_,_) -> loc | GSort (loc,_) -> loc - | GHole (loc,_,_) -> loc + | GHole (loc,_,_,_) -> loc | GCast (loc,_,_) -> loc (**********************************************************************) @@ -356,7 +357,7 @@ let rec cases_pattern_of_glob_constr na = function raise Not_found | Anonymous -> PatVar (loc,Name id) end - | GHole (loc,_,_) -> PatVar (loc,na) + | GHole (loc,_,_,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr,_) -> PatCstr (loc,cstr,[],na) | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> |