diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 18:05:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 18:05:13 +0000 |
| commit | 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 (patch) | |
| tree | fc18af5b3330e830a8e979bc551db46b25bda05d /plugins/subtac/subtac_cases.ml | |
| parent | cb2f5d06481f9021f600eaefbdc6b33118bd346d (diff) | |
A bit of cleaning around name generation + creation of dedicated file namegen.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac_cases.ml')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 4eb05df74..bc4d834d4 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -15,6 +15,7 @@ open Names open Nameops open Term open Termops +open Namegen open Declarations open Inductiveops open Environ @@ -1501,7 +1502,7 @@ let make_prime_id name = let prime avoid name = let previd, id = make_prime_id name in - previd, next_ident_away_from id avoid + previd, next_ident_away id avoid let make_prime avoid prevname = let previd, id = prime !avoid prevname in @@ -1510,7 +1511,7 @@ let make_prime avoid prevname = let eq_id avoid id = let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away_from hid avoid in + let hid' = next_ident_away hid avoid in hid' let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) @@ -1588,7 +1589,7 @@ let constr_of_pat env isevars arsign pat avoid = (* shadows functional version *) let eq_id avoid id = let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away_from hid !avoid in + let hid' = next_ident_away hid !avoid in avoid := hid' :: !avoid; hid' @@ -1784,7 +1785,7 @@ let abstract_tomatch env tomatchs tycon = | _ -> let tycon = Option.map (fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in - let name = next_ident_away_from (id_of_string "filtered_var") names in + let name = next_ident_away (id_of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, name :: names, tycon) |