From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Dec 2006 10:43:54 +0000 (+0000)
Subject: Collapse_head_metas transforms all terms "not-recongnized" into a
X-Git-Tag: make_still_working~6569
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=002ad23d3995439a265b9879432a30835b8d3395;p=helm.git

Collapse_head_metas transforms all terms "not-recongnized" into a
meta.
---

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 1de149270..c8d370f04 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/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 =