From d0a8a10b94687500347e677bcfd14b0016c775b4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Dec 2006 10:43:54 +0000 Subject: [PATCH] Collapse_head_metas transforms all terms "not-recongnized" into a meta. --- components/tactics/universe.ml | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml index 1de149270..c8d370f04 100644 --- a/components/tactics/universe.ml +++ b/components/tactics/universe.ml @@ -44,15 +44,31 @@ let rec unfold context = function Cic.Prod(name,s,t') | t -> ProofEngineReduction.unfold context t -let rec collapse_head_metas = function - | Cic.Appl(a::l) -> - let a' = collapse_head_metas a in - (match a' with - | Cic.Meta(n,m) -> Cic.Meta(n,m) - | t -> - let l' = List.map collapse_head_metas l in - Cic.Appl(t::l')) - | t -> t +let rec collapse_head_metas t = + match t with + | Cic.Appl([]) -> assert false + | Cic.Appl(a::l) -> + let a' = collapse_head_metas a in + (match a' with + | Cic.Meta(n,m) -> Cic.Meta(n,m) + | t -> + let l' = List.map collapse_head_metas l in + Cic.Appl(t::l')) + | Cic.Rel _ + | Cic.Var _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ + | Cic.Const _ + | Cic.MutInd _ + | Cic.MutConstruct _ -> t + | Cic.LetIn _ + | Cic.Lambda _ + | Cic.Prod _ + | Cic.Cast _ + | Cic.MutCase _ + | Cic.Fix _ + | Cic.CoFix _ -> Cic.Meta(-1,[]) ;; let rec dummies_of_coercions = -- 2.39.2