From fdea894deb3813f1103b0607b5e3854d501d82da Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Dec 2006 10:30:59 +0000 Subject: [PATCH] The function uri_of_term now works also if the explciit substitution list is not empty. --- helm/software/components/cic/cicUtil.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 6e07a4995..31b47f672 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -61,7 +61,8 @@ let clean_up_local_context subst metasenv n l = None , _ -> None | _ , t -> t) cc l with - Invalid_argument _ -> assert false) + Invalid_argument _ -> + assert false) let is_closed = let module C = Cic in @@ -165,12 +166,12 @@ let term_of_uri uri = | Not_found -> raise (UriManager.IllFormedUri s) let uri_of_term = function - | Cic.Const (uri, []) - | Cic.Var (uri, []) -> uri - | Cic.MutInd (baseuri, tyno, []) -> + | Cic.Const (uri, _) + | Cic.Var (uri, _) -> uri + | Cic.MutInd (baseuri, tyno, _) -> UriManager.uri_of_string (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1)) - | Cic.MutConstruct (baseuri, tyno, consno, []) -> + | Cic.MutConstruct (baseuri, tyno, consno, _) -> UriManager.uri_of_string (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri) (tyno + 1) consno) -- 2.39.2