diff options
| author | ppedrot | 2013-08-03 18:35:03 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-03 18:35:03 +0000 |
| commit | 2b8ad61822111fad93176b54800cb43e347df292 (patch) | |
| tree | 9a4668cc5533d355a69c3f6583658ee9e342c66b /tactics | |
| parent | eb4bdf9317ad53f464a87219c1625b9118d4660a (diff) | |
Replacing uses of association lists by maps in notations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index eca9c7716c..b397bcaa3f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -305,7 +305,7 @@ let intern_binding_name ist x = let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in - let ltacvars = (Id.Set.elements lfun, Id.Set.empty) in + let ltacvars = (lfun, Id.Set.empty) in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c in @@ -378,7 +378,7 @@ let intern_flag ist red = let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_constr_pattern ist ~as_type ~ltacvars pc = - let ltacvars = Id.Set.elements ltacvars, Id.Set.empty in + let ltacvars = ltacvars, Id.Set.empty in let metas,pat = Constrintern.intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 14c8c8f662..30813d5306 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -478,9 +478,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = context at globalization time: we retype with the now known intros/lettac/inversion hypothesis names *) | Some c -> - let fold id _ accu = id :: accu in - let ltacvars = Id.Map.fold fold constrvars [] in - let bndvars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in + let fold id _ accu = Id.Set.add id accu in + let ltacvars = Id.Map.fold fold constrvars Id.Set.empty in + let bndvars = Id.Map.fold fold ist.lfun Id.Set.empty in let ltacdata = (ltacvars, bndvars) in intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c in |