| C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
| C.Appl l -> C.Appl (List.map (unwind_aux m) 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,_) -> reduce (0, [], body, s)
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | (k, e, (C.Abst _ as t), s) -> t (* s should be empty ????? *)
| (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in
if s = [] then t' else C.Appl (t'::s)
| (k, e, (C.MutConstruct (uri,_,_,_) as t),s) ->
eat_first (num_to_eat,tl)
in
reduce (k, e, (List.nth pl (j-1)),(ts@s))
- | C.Abst _| C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ -> let t' = unwind k e t in
if s = [] then t' else C.Appl (t'::s)
| C.Appl [] -> raise (Impossible 1)
| C.Appl (he::tl) -> reduce (0, [], he, tl)
| C.Const _ as t -> reduce (0, [], t, [])
- | C.Abst _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase _ as t -> reduce (0, [], t, [])