-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
| 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') ->
(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) ->
| 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) ->
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
exception WrongShape;;
exception AlreadySimplified;;
-exception WhatShouldIDo;;
(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
(* superfluous *)
aux (he::rev_constant_args) tl (S.subst he t)
end
- | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
+ | C.LetIn (_,s,t) ->
+ aux rev_constant_args l (S.subst s t)
| C.Fix (i,fl) as t ->
let tys =
List.map (function (name,_,ty,_) ->
| 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) ->
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