diff options
| author | herbelin | 2000-10-04 13:36:20 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-04 13:36:20 +0000 |
| commit | ba753cf3c13ec88cfc1210c0f297b88cc58e5e14 (patch) | |
| tree | c63264a863f1d586f08087fc71a8dba48f35846d | |
| parent | 736e19d7cb974952ac1e7b133476a15f0d2e1147 (diff) | |
code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@645 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 07219dd359..dcf09b5f1d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1169,27 +1169,6 @@ let decomp_tuple_term env c t = in List.split (decomprec (mkRel 1) c t) -(* -let whd_const_state namelist env sigma = - let rec whrec (x, l as s) = - match kind_of_term x with - | IsConst (sp,_) when List.mem sp namelist -> - if evaluable_constant env x then - whrec (constant_value env x, l) - else - error "whd_const_stack" - | IsCast (c,_) -> whrec (c, l) - | IsApp (f,cl) -> whrec (f, append_stack cl l) - | _ -> s - in - whrec -let whd_const_state namelist = whd_state (const namelist) -let whd_const_stack namelist env sigma x = - whd_const_state namelist env sigma (x, empty_stack) -let whd_const namelist env sigma c = - app_stack (whd_const_stack namelist env sigma (c, empty_stack)) -*) - let subst_tuple_term env sigma dep_pair b = let typ = get_type_of env sigma dep_pair in let e_list,proj_list = decomp_tuple_term env dep_pair typ in |