* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO unify exceptions *)
exception CicReductionInternalError;;
let t = whd ~delta ~subst ctx term in
let aux = normalize ~delta ~subst in
let decl name t = Some (name, C.Decl t) in
- let def name t = Some (name, C.Def (t,None)) in
match t with
| C.Rel n -> t
| C.Var (uri,exp_named_subst) ->