diff options
| author | Hugo Herbelin | 2014-06-03 14:23:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-04 18:42:22 +0200 |
| commit | 6c9e2ded8fc093e42902d008a883b6650533d47f (patch) | |
| tree | 53b91966c76b3a535308a8a73d113c5fff96de0a /tactics | |
| parent | 90fc6f45fa1a4ef5251046d8b4e4249164afa60b (diff) | |
Collecting in Namegen those conventional default names that are used in different places
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
3 files changed, 4 insertions, 7 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index ab2a165757..bcf5e29476 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -888,7 +888,7 @@ type hints_entry = | HintsExternEntry of int * (patvar list * constr_pattern) option * glob_tactic_expr -let h = Id.of_string "H" +let default_prepare_hint_ident = Id.of_string "H" exception Found of constr * types @@ -915,7 +915,7 @@ let prepare_hint check env init (sigma,c) = let rec iter c = try find_next_evar c; c with Found (evar,t) -> - let id = next_ident_away_from h (fun id -> Id.Set.mem id !vars) in + let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in vars := Id.Set.add id !vars; subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index abf1c47d84..1e88456f36 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -482,7 +482,7 @@ let rec decompose_app_rel env evd t = else let (f', args) = decompose_app_rel env evd args.(0) in let ty = Typing.type_of env evd args.(0) in - let f'' = mkLambda (Name (Id.of_string "x"), ty, + let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', args) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index afd077e64a..e08ae998b4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -432,11 +432,8 @@ let id_of_name_with_default id = function | Anonymous -> id | Name id -> id -let hid = Id.of_string "H" -let xid = Id.of_string "X" - let default_id_of_sort s = - if Sorts.is_small s then hid else xid + if Sorts.is_small s then default_small_ident else default_type_ident let default_id env sigma = function | (name,None,t) -> |