* Abst removed from the DTD

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 460c8d7263acfbeed94a2536fa3cfd5c6abb8cad..941a701a920df3b6424fa504efbfecd89e076ab2 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -75,7 +75,6 @@ let rec syntactic_equality t t' =
     | C.Appl l, C.Appl l' ->
        List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
     | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
-    | C.Abst _, C.Abst _ -> assert false
     | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
        UriManager.eq uri uri' && i = i'
     | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
@@ -124,7 +123,6 @@ let replace ~equality ~what ~with_what ~where =
            (C.Appl l')::tl -> C.Appl (l'@tl)
          | l' -> C.Appl l')
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -203,7 +201,6 @@ let reduce context =
          | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
@@ -265,7 +262,7 @@ let reduce context =
                  eat_first (num_to_eat,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in
@@ -483,7 +480,6 @@ let simpl context =
          | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
@@ -543,7 +539,7 @@ let simpl context =
                  eat_first (num_to_eat,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in