diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 19:55:01 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 19:55:01 +0000 |
commit | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (patch) | |
tree | acd60ed341ff45754de77090e1791bbc4718898e /proofs | |
parent | dcfeca5f828bc2648b567616e3dfabd03e13d9ab (diff) |
Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenv.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f78ab9611..f2c7d0f14 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -265,17 +265,17 @@ let unify m gls = let collect_metas c = let rec collrec acc c = - match splay_constr c with - | OpMeta mv, _ -> mv::acc - | _, cl -> Array.fold_left collrec acc cl + match kind_of_term c with + | IsMeta mv -> mv::acc + | _ -> fold_constr collrec acc c in List.rev (collrec [] c) let metavars_of c = let rec collrec acc c = - match splay_constr c with - | OpMeta mv, _ -> Intset.add mv acc - | _, cl -> Array.fold_left collrec acc cl + match kind_of_term c with + | IsMeta mv -> Intset.add mv acc + | _ -> fold_constr collrec acc c in collrec Intset.empty c |