+ let sequent =
+ let i,canonical_context,term = sequent in
+ let canonical_context' =
+ List.fold_right
+ (fun d canonical_context' ->
+ let d' =
+ match d with
+ None -> None
+ | Some (n, Cic.Decl t)->
+ Some (n, Cic.Decl (Unshare.unshare t))
+ | Some (n, Cic.Def (t,None)) ->
+ Some (n,
+ Cic.Def ((Unshare.unshare t),None))
+ | Some (_,Cic.Def (_,Some _)) -> assert false
+ in
+ d::canonical_context'
+ ) [] canonical_context
+ in
+ let term' = Unshare.unshare term in
+ (i,canonical_context',term')
+ in