diff options
author | 2009-09-17 15:58:14 +0000 | |
---|---|---|
committer | 2009-09-17 15:58:14 +0000 | |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /tactics/termdn.ml | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/termdn.ml')
-rw-r--r-- | tactics/termdn.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 591b2947c..32e65239d 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -25,20 +25,20 @@ type 'a t = (global_reference,constr_pattern,'a) Dn.t (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*) -let decomp = +let decomp = let rec decrec acc c = match kind_of_term c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) - in + in decrec [] -let decomp_pat = +let decomp_pat = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f | c -> (c,acc) - in - decrec [] + in + decrec [] let constr_pat_discr t = if not (occur_meta_pattern t) then @@ -54,7 +54,7 @@ let constr_pat_discr_st (idpred,cpred) t = match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args) - | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> + | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> Some(ref,args) | PVar v, args when not (Idpred.mem v idpred) -> Some(VarRef v,args) @@ -64,7 +64,7 @@ let constr_pat_discr_st (idpred,cpred) t = open Dn -let constr_val_discr t = +let constr_val_discr t = let c, l = decomp t in match kind_of_term c with | Ind ind_sp -> Label(IndRef ind_sp,l) @@ -72,8 +72,8 @@ let constr_val_discr t = | Var id -> Label(VarRef id,l) | Const _ -> Everything | _ -> Nothing - -let constr_val_discr_st (idpred,cpred) t = + +let constr_val_discr_st (idpred,cpred) t = let c, l = decomp t in match kind_of_term c with | Const c -> if Cpred.mem c cpred then Everything else Label(ConstRef c,l) @@ -83,12 +83,12 @@ let constr_val_discr_st (idpred,cpred) t = | Evar _ -> Everything | _ -> Nothing -let create = Dn.create +let create = Dn.create let add dn st = Dn.add dn (constr_pat_discr_st st) let rmv dn st = Dn.rmv dn (constr_pat_discr_st st) let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t - + let app f dn = Dn.app f dn |