| Ast.Magic _
| Ast.Variable _) as t -> special_k t
| (Ast.Ident _
- | Ast.Implicit
+ | Ast.NRef _
+ | Ast.NCic _
+ | Ast.Implicit _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
| Ast.Ident (_, Some substs) -> aux_substs substs
| Ast.Meta (_, substs) -> aux_meta_substs substs
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | Ast.UriPattern uri -> uri :: acc
+ | Ast.UriPattern uri -> `Uri uri :: acc
+ | Ast.NRefPattern nref -> `NRef nref :: acc
| Ast.ImplicitPattern
| Ast.VarPattern _ -> acc
| Ast.ApplPattern apl -> List.fold_left aux acc apl
in
let uris = aux [] ap in
- HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
+ let cmp u1 u2 =
+ match u1,u2 with
+ `Uri u1, `Uri u2 -> UriManager.compare u1 u2
+ | `NRef r1, `NRef r2 -> NReference.compare r1 r2
+ | `Uri _,`NRef _ -> -1
+ | `NRef _, `Uri _ -> 1
+ in
+ HExtlib.list_uniq (List.fast_sort cmp uris)
let rec find_branch =
function
!fresh_index
(* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "η" ^ string_of_int (fresh_id ())
+ (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
indtypes
in
CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
- | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
+ | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
- CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
+ CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
| CicNotationPt.Record (params, n, ty, fields) ->
CicNotationPt.Record (freshen_capture_variables params, n,
freshen_term ty, freshen_name_ty_b fields)