1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let unshare ?(fresh_univs=false) t =
33 | C.Var (uri,exp_named_subst) ->
34 let exp_named_subst' =
35 List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst
37 C.Var (uri,exp_named_subst')
43 | Some t -> Some (unshare t)
47 | C.Sort s when not fresh_univs -> C.Sort s
48 | C.Sort (C.Type _) -> C.Sort (C.Type (CicUniv.fresh ()))
49 | C.Sort s -> C.Sort s
50 | C.Implicit info -> C.Implicit info
51 | C.Cast (te,ty) -> C.Cast (unshare te, unshare ty)
52 | C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t)
53 | C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t)
54 | C.LetIn (n,s,ty,t) ->
55 C.LetIn (n, unshare s, unshare ty, unshare t)
56 | C.Appl l -> C.Appl (List.map unshare l)
57 | C.Const (uri,exp_named_subst) ->
58 let exp_named_subst' =
59 List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst
61 C.Const (uri,exp_named_subst')
62 | C.MutInd (uri,tyno,exp_named_subst) ->
63 let exp_named_subst' =
64 List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst
66 C.MutInd (uri,tyno,exp_named_subst')
67 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
68 let exp_named_subst' =
69 List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst
71 C.MutConstruct (uri,tyno,consno,exp_named_subst')
72 | C.MutCase (sp,i,outty,t,pl) ->
73 C.MutCase (sp, i, unshare outty, unshare t,
78 (fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo))
85 (fun (name, ty, bo) -> (name, unshare ty, unshare bo))