- let buri = UriManager.buri_of_uri uri in
- let index = String.rindex buri '/' in
- let filename = String.sub buri (index + 1) (String.length buri - index - 1) in
- if current_module_name = filename then
+ let filename =
+ let suri = UriManager.buri_of_uri uri in
+ let s = String.sub suri 5 (String.length suri - 5) in
+ let s = Pcre.replace ~pat:"/" ~templ:"_" s in
+ String.uncapitalize s in
+ if current_module_uri = UriManager.buri_of_uri uri then
(* pretty-prints a term t of cic in an environment l where l is a list of *)
(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
(* name associated to the greatest DeBrujin index in t *)
(* pretty-prints a term t of cic in an environment l where l is a list of *)
(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
(* name associated to the greatest DeBrujin index in t *)
NotEnoughElements -> string_of_int (List.length context - n)
end
| C.Var (uri,exp_named_subst) ->
NotEnoughElements -> string_of_int (List.length context - n)
end
| C.Var (uri,exp_named_subst) ->
| C.Appl li ->
"(" ^ String.concat " " (clean_args context li) ^ ")"
| C.Const (uri,exp_named_subst) ->
| C.Appl li ->
"(" ^ String.concat " " (clean_args context li) ^ ")"
| C.Const (uri,exp_named_subst) ->
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
(* ppinductiveType (typename, inductive, arity, cons) *)
(* pretty-prints a single inductive definition *)
(* (typename, inductive, arity, cons) *)
(* ppinductiveType (typename, inductive, arity, cons) *)
(* pretty-prints a single inductive definition *)
(* (typename, inductive, arity, cons) *)
-let ppinductiveType current_module_name nparams (typename, inductive, arity, cons)
+let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
match obj with
C.Constant (name, Some t1, t2, params, _) ->
(match analyze_type [] t2 with
match obj with
C.Constant (name, Some t1, t2, params, _) ->
(match analyze_type [] t2 with
let abstr =
let s = String.concat "," abstr in
if s = "" then "" else "(" ^ s ^ ") "
let abstr =
let s = String.concat "," abstr in
if s = "" then "" else "(" ^ s ^ ") "
pp ~metasenv:conjectures ty []
| C.InductiveDefinition (l, params, nparams, _) ->
List.fold_right
pp ~metasenv:conjectures ty []
| C.InductiveDefinition (l, params, nparams, _) ->
List.fold_right