now destruct takes an optional list of term rather than a sigle optional term

[helm.git] / components / tactics / universe.ml

diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml
index 40c3c1abdbb560ed2b5c20586aeca44d520509bf..99041ed1ba33a8e1e526d1e96656f7c13a612046 100644 (file)
--- a/components/tactics/universe.ml
+++ b/components/tactics/universe.ml
@@ -41,42 +41,59 @@ let get_candidates univ ty =
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
-       Cic.Prod(name,s,t')     
+        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 = 
   function
-    | Cic.Appl (c::l) when CoercGraph.is_a_coercion c ->
-       Cic.Meta (-1,[])
+    | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+        Cic.Meta (-1,[])
     | Cic.Appl l -> 
-       let l' = List.map dummies_of_coercions l in Cic.Appl l'
+        let l' = List.map dummies_of_coercions l in Cic.Appl l'
     | Cic.Lambda(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.Lambda (n,s',t')
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Lambda (n,s',t')
     | Cic.Prod(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.Prod (n,s',t')    
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Prod (n,s',t')        
     | Cic.LetIn(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.LetIn (n,s',t')   
-    | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[])
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.LetIn (n,s',t')        
+    | Cic.MutCase _ -> Cic.Meta (-1,[])
     | t -> t
 ;;
 
+
 let rec head remove_coercions t = 
   let clean_up t =
     if remove_coercions then dummies_of_coercions t
@@ -93,7 +110,7 @@ let index univ key term =
   (* flexible terms are not indexed *)
   if key = Cic.Meta(-1,[]) then univ
   else
-    (prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
+    ((*prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);*)
      TI.index univ key term)
 ;;
 
@@ -102,6 +119,8 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
+let key term = head false term
+
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
   let univ = index univ key t in