* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let rec unshare =
let module C = Cic in
function
) l
in
C.Meta(i,l')
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
+ | C.Sort s -> C.Sort s
+ | C.Implicit info -> C.Implicit info
| C.Cast (te,ty) -> C.Cast (unshare te, unshare ty)
| C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t)
| C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t)
C.MutCase (sp, i, unshare outty, unshare t,
List.map unshare pl)
| C.Fix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo))
in
C.Fix (i, liftedfl)
| C.CoFix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, ty, bo) -> (name, unshare ty, unshare bo))