aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml5
-rw-r--r--interp/constrintern.ml119
-rw-r--r--interp/topconstr.ml4
-rw-r--r--interp/topconstr.mli4
-rw-r--r--library/impargs.ml86
-rw-r--r--library/impargs.mli2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_constrnew.ml428
-rw-r--r--parsing/ppconstr.ml3
-rw-r--r--parsing/prettyp.ml24
-rw-r--r--parsing/q_coqast.ml46
-rw-r--r--translate/ppconstrnew.ml10
12 files changed, 205 insertions, 88 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 88e419fa6..ec9e88c77 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -378,7 +378,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CFix _ -> assert false
and xlate_formula_expl = function
(a, None) -> xlate_formula a
- | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a)
+ | (a, Some (_,ExplByPos i)) ->
+ CT_bang(xlate_int_opt (Some i), xlate_formula a)
+ | (a, Some (_,ExplByName i)) ->
+ xlate_error "TODO: explicitation of implicit by name"
and xlate_formula_expl_ne_list = function
[] -> assert false
| a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c07522cc7..d1ce06712 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -47,7 +47,7 @@ type internalisation_error =
| UnboundFixName of bool * identifier
| NonLinearPattern of identifier
| BadPatternsNumber of int * int
- | BadExplicitationNumber of int * int option
+ | BadExplicitationNumber of explicitation * int option
exception InternalisationError of loc * internalisation_error
@@ -78,11 +78,19 @@ let explain_bad_patterns_number n1 n2 =
++ int n2
let explain_bad_explicitation_number n po =
- let s = match po with
- | None -> "a regular argument"
- | Some p -> string_of_int p in
- str "Bad explicitation number: found " ++ int n ++
- str" but was expecting " ++ str s
+ match n with
+ | ExplByPos n ->
+ let s = match po with
+ | None -> str "a regular argument"
+ | Some p -> int p in
+ str "Bad explicitation number: found " ++ int n ++
+ str" but was expecting " ++ s
+ | ExplByName id ->
+ let s = match po with
+ | None -> str "a regular argument"
+ | Some p -> (*pr_id (name_of_position p) in*) failwith "" in
+ str "Bad explicitation name: found " ++ pr_id id ++
+ str" but was expecting " ++ s
let explain_internalisation_error = function
| VariableCapture id -> explain_variable_capture id
@@ -394,7 +402,6 @@ let push_name_env (ids,impls,tmpsc,scopes as env) = function
(**********************************************************************)
(* Utilities for application *)
-
let check_projection isproj nargs r =
match (r,isproj) with
| RRef (loc, ref), Some nth ->
@@ -413,6 +420,41 @@ let set_hole_implicit i = function
| RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
| _ -> anomaly "Only refs have implicits"
+let exists_implicit_name id =
+ List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp)
+
+let extract_explicit_arg imps args =
+ let rec aux = function
+ | [] -> [],[]
+ | (a,e)::l ->
+ let (eargs,rargs) = aux l in
+ match e with
+ | None -> (eargs,a::rargs)
+ | Some (loc,pos) ->
+ let id = match pos with
+ | ExplByName id ->
+ if not (exists_implicit_name id imps) then
+ user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id);
+ if List.mem_assoc id eargs then
+ user_err_loc (loc,"",str "Argument name " ++ pr_id id
+ ++ str " occurs more than once");
+ id
+ | ExplByPos p ->
+ let id =
+ try
+ let imp = List.nth imps (p-1) in
+ if not (is_status_implicit imp) then failwith "imp";
+ name_of_implicit imp
+ with Failure _ (* "nth" | "imp" *) ->
+ user_err_loc (loc,"",str"Wrong argument position: " ++ int p)
+ in
+ if List.mem_assoc id eargs then
+ user_err_loc (loc,"",str"Argument at position " ++ int p ++
+ str " is mentioned more than once");
+ id in
+ ((id,(loc,a))::eargs,rargs)
+ in aux args
+
(**********************************************************************)
(* Syntax extensions *)
@@ -628,39 +670,38 @@ let internalise sigma env allow_soapp lvar c =
| [] -> intern env body
and intern_impargs c env l subscopes args =
- let rec aux n l subscopes args =
+ let eargs, rargs = extract_explicit_arg l args in
+ let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
- match (l,args) with
- | (imp::l', (a,Some j)::args') ->
- if is_status_implicit imp & j>=n then
- if j=n then
- (intern enva a)::(aux (n+1) l' subscopes' args')
- else
- (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
- else
- let e = if is_status_implicit imp then Some n else None in
- raise
- (InternalisationError(constr_loc a,BadExplicitationNumber (j,e)))
- | (imp::l',(a,None)::args') ->
- if is_status_implicit imp then
- (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
- else
- (intern enva a)::(aux (n+1) l' subscopes' args')
- | ([],args) -> intern_tailargs env subscopes args
- | (_::l',[]) ->
- if List.for_all is_status_implicit l then
- (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes args)
- else []
- in
- aux 1 l subscopes args
-
- and intern_tailargs env subscopes = function
- | (a,Some _)::args' ->
- raise (InternalisationError (constr_loc a, WrongExplicitImplicit))
- | (a,None)::args ->
- let (enva,subscopes) = apply_scope_env env subscopes in
- (intern enva a) :: (intern_tailargs env subscopes args)
- | [] -> []
+ match (impl,rargs) with
+ | (imp::impl', rargs) when is_status_implicit imp ->
+ begin try
+ let id = name_of_implicit imp in
+ let (_,a) = List.assoc id eargs in
+ let eargs' = List.remove_assoc id eargs in
+ intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
+ with Not_found ->
+ if rargs=[] & eargs=[] &
+ not (List.for_all is_status_implicit impl') then
+ (* Less regular arguments than expected: don't complete *)
+ (* with implicit arguments *)
+ []
+ else
+ RHole (set_hole_implicit n c) ::
+ aux (n+1) impl' subscopes' eargs rargs
+ end
+ | (imp::impl', a::rargs') ->
+ intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
+ | (imp::impl', []) ->
+ if eargs <> [] then
+ (let (id,(loc,_)) = List.hd eargs in
+ user_err_loc (loc,"",str "Not enough non implicit
+ arguments to accept the argument bound to " ++ pr_id id));
+ []
+ | ([], rargs) ->
+ assert (eargs = []);
+ intern_args env subscopes rargs
+ in aux 1 l subscopes eargs rargs
and intern_args env subscopes = function
| [] -> []
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c3b44b9e2..084883349 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -400,7 +400,7 @@ let match_aconstr c (metas_scl,pat) =
type notation = string
-type explicitation = int
+type explicitation = ExplByPos of int | ExplByName of identifier
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -421,7 +421,7 @@ type constr_expr =
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
- (constr_expr * explicitation option) list
+ (constr_expr * explicitation located option) list
| CCases of loc * (constr_expr option * constr_expr option) *
(constr_expr * (name * (loc * reference * name list) option)) list *
(loc * cases_pattern_expr list * constr_expr) list
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1636edfd3..a4b20b65c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -63,7 +63,7 @@ val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
type notation = string
-type explicitation = int
+type explicitation = ExplByPos of int | ExplByName of identifier
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -84,7 +84,7 @@ type constr_expr =
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
- (constr_expr * explicitation option) list
+ (constr_expr * explicitation located option) list
| CCases of loc * (constr_expr option * constr_expr option) *
(constr_expr * (name * (loc * reference * name list) option)) list *
(loc * cases_pattern_expr list * constr_expr) list
diff --git a/library/impargs.ml b/library/impargs.ml
index 224d1cc76..f2c37374d 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -19,6 +19,7 @@ open Inductive
open Libobject
open Lib
open Nametab
+open Pp
(*s Flags governing the computation of implicit arguments *)
@@ -122,7 +123,7 @@ let argument_less = function
| Hyp _, Conclusion -> true
| Conclusion, _ -> false
-let update pos rig st =
+let update pos rig (na,st) =
let e =
if rig then
match st with
@@ -146,7 +147,7 @@ let update pos rig st =
| Some (DepFlex fpos as x) ->
if argument_less (pos,fpos) then DepFlex pos else x
| Some Manual -> assert false
- in Some e
+ in na, Some e
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env bound depth f =
@@ -207,29 +208,41 @@ let add_free_rels_until strict bound env m pos acc =
(* calcule la liste des arguments implicites *)
-let compute_implicits output env t =
- let strict =
- if output then !strict_implicit_args_out else !strict_implicit_args in
- let rec aux env n t =
+let compute_implicits_gen strict contextual env t =
+ let rec aux env n names t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
| Prod (x,a,b) ->
add_free_rels_until strict n env a (Hyp (n+1))
- (aux (push_rel (x,None,a) env) (n+1) b)
+ (aux (push_rel (x,None,a) env) (n+1) (x::names) b)
| _ ->
- let v = Array.create n None in
- if (not output & !contextual_implicit_args) or
- (output & !contextual_implicit_args_out)
- then
- add_free_rels_until strict n env t Conclusion v
+ let names = List.rev names in
+ let v = Array.map (fun na -> na,None) (Array.of_list names) in
+ if contextual then add_free_rels_until strict n env t Conclusion v
else v
in
match kind_of_term (whd_betadeltaiota env t) with
| Prod (x,a,b) ->
- Array.to_list (aux (push_rel (x,None,a) env) 1 b)
+ let v = aux (push_rel (x,None,a) env) 1 [x] b in
+ Array.to_list v
| _ -> []
-type implicit_status = implicit_explanation option (* None = Not implicit *)
+let compute_implicits output env t =
+ let strict =
+ (not output & !strict_implicit_args) or
+ (output & !strict_implicit_args_out) in
+ let contextual =
+ (not output & !contextual_implicit_args) or
+ (output & !contextual_implicit_args_out) in
+ let l = compute_implicits_gen strict contextual env t in
+ List.map (function
+ | (Name id, Some imp) -> Some (id,imp)
+ | (Anonymous, Some _) -> anomaly "Unnamed implicit"
+ | _ -> None) l
+
+type implicit_status =
+ (* None = Not implicit *)
+ (identifier * implicit_explanation) option
type implicits_list = implicit_status list
@@ -237,22 +250,26 @@ let is_status_implicit = function
| None -> false
| _ -> true
+let name_of_implicit = function
+ | None -> anomaly "Not an implicit argument"
+ | Some (id,_) -> id
+
(* [in_ctx] means we now the expected type, [n] is the index of the argument *)
let is_inferable_implicit in_ctx n = function
| None -> false
- | Some (DepRigid (Hyp p)) -> n >= p
- | Some (DepFlex (Hyp p)) -> false
- | Some (DepFlexAndRigid (_,Hyp q)) -> n >= q
- | Some (DepRigid Conclusion) -> in_ctx
- | Some (DepFlex Conclusion) -> false
- | Some (DepFlexAndRigid (_,Conclusion)) -> false
- | Some Manual -> true
+ | Some (_,DepRigid (Hyp p)) -> n >= p
+ | Some (_,DepFlex (Hyp p)) -> false
+ | Some (_,DepFlexAndRigid (_,Hyp q)) -> n >= q
+ | Some (_,DepRigid Conclusion) -> in_ctx
+ | Some (_,DepFlex Conclusion) -> false
+ | Some (_,DepFlexAndRigid (_,Conclusion)) -> false
+ | Some (_,Manual) -> true
let positions_of_implicits =
let rec aux n = function
[] -> []
- | Some _::l -> n :: aux (n+1) l
- | None::l -> aux (n+1) l
+ | Some _ :: l -> n :: aux (n+1) l
+ | None :: l -> aux (n+1) l
in aux 1
type strict_flag = bool (* true = strict *)
@@ -421,17 +438,28 @@ let implicits_of_global_out r =
let check_range n i =
if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+
let declare_manual_implicits r l =
let t = Global.type_of_global r in
- let n = List.length (fst (dest_prod (Global.env()) t)) in
+ let autoimps = compute_implicits_gen false true (Global.env()) t in
+ let n = List.length autoimps in
if not (list_distinct l) then error ("Some numbers occur several time");
List.iter (check_range n) l;
let l = List.sort (-) l in
- let rec aux k = function
- | [] -> if k>n then [] else None :: aux (k+1) []
- | p::l as l' ->
- if k=p then Some Manual :: aux (k+1) l else None :: aux (k+1) l' in
- let l = Impl_manual (aux 1 l) in
+ (* Compare with automatic implicits to recover printing data and names *)
+ let rec merge k = function
+ | [], [] -> []
+ | ((na,imp)::imps, p::l) when k=p ->
+ let id = match na with
+ | Name id -> id
+ | _ -> errorlabstrm ""
+ (str "Cannot set implicit argument number " ++ int p ++
+ str ": it has no name") in
+ let imp = match imp with None -> (id,Manual) | Some imp -> (id,imp) in
+ Some imp :: merge (k+1) (imps,l)
+ | _::imps, l' -> None :: merge (k+1) (imps,l')
+ | [], _ -> assert false in
+ let l = Impl_manual (merge 1 (autoimps,l)) in
let (_,oimp_out) = implicits_of_global_gen r in
let l = l, if !Options.v7_only then oimp_out else l in
add_anonymous_leaf (in_implicits [r,l])
diff --git a/library/impargs.mli b/library/impargs.mli
index e0e362369..83ca8dfb9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -37,6 +37,8 @@ type implicits_list = implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
+val name_of_implicit : implicit_status -> identifier
+
val positions_of_implicits : implicits_list -> int list
(* Computation of the positions of arguments automatically inferable
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 16e1a6388..43879c3b6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -217,7 +217,7 @@ GEXTEND Gram
;
constr91:
[ [ test_int_bang; n = INT; "!"; c = operconstr LEVEL "9" ->
- (c, Some (int_of_string n))
+ (c, Some (loc,ExplByPos (int_of_string n)))
| c = operconstr LEVEL "9" -> (c, None) ] ]
;
(* annot and product_annot_tail are hacks to forbid concrete syntax *)
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 6e279218e..c3a7c27b3 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -132,10 +132,27 @@ let rec mkCLambdaN loc bll c =
| [] -> c
| LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
+(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
+(* admissible notation "(n)" *)
+let test_lpar_id_coloneq =
+ Gram.Entry.of_parser "test_lpar_id_coloneq"
+ (fun strm ->
+ match Stream.npeek 1 strm with
+ | [("", "(")] ->
+ begin match Stream.npeek 2 strm with
+ | [_; ("IDENT", _)] ->
+ begin match Stream.npeek 3 strm with
+ | [_; _; ("", ":=")] -> ()
+ | _ -> raise Stream.Failure
+ end
+ | _ -> raise Stream.Failure
+ end
+ | _ -> raise Stream.Failure)
+
if not !Options.v7 then
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
- constr_pattern Constr.ident binder_let tuple_constr;
+ constr_pattern lconstr_pattern Constr.ident binder_let tuple_constr;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -151,6 +168,9 @@ GEXTEND Gram
constr_pattern:
[ [ c = constr -> c ] ]
;
+ lconstr_pattern:
+ [ [ c = lconstr -> c ] ]
+ ;
sort:
[ [ "Set" -> RProp Pos
| "Prop" -> RProp Null
@@ -218,7 +238,11 @@ GEXTEND Gram
| c=fix_constr -> c ] ]
;
appl_arg:
- [ [ "@"; n=INT; ":="; c=constr -> (c,Some(int_of_string n))
+ [ [ _ = test_lpar_id_coloneq; "("; id = ident; ":="; c=lconstr; ")" ->
+ (c,Some (loc,ExplByName id))
+(*
+ | "@"; n=INT; ":="; c=constr -> (c,Some(loc,ExplByPos (int_of_string n)))
+*)
| c=constr -> (c,None) ] ]
;
atomic_constr:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index af651a4f2..4afdf55f4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -81,7 +81,8 @@ let pr_sort = function
let pr_explicitation = function
| None -> mt ()
- | Some n -> int n ++ str "!"
+ | Some (_,ExplByPos n) -> int n ++ str "!"
+ | Some (_,ExplByName n) -> anomaly "Argument made explicit by name"
let pr_expl_args pr (a,expl) =
pr_explicitation expl ++ pr (lapp,L) a
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bf26f02ec..d39be3919 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -47,7 +47,19 @@ let print_impl_args_by_pos = function
prlist_with_sep (fun () -> str "; ") int l ++
str"] are implicit" ++ fnl()
-let print_impl_args l = print_impl_args_by_pos (positions_of_implicits l)
+let print_impl_args_by_name = function
+ | [] -> mt ()
+ | [i] -> str"Argument " ++ pr_id (name_of_implicit i) ++ str" is implicit" ++
+ fnl()
+ | l ->
+ str"Arguments " ++
+ prlist_with_sep (fun () -> str ", ")
+ (fun imp -> pr_id (name_of_implicit imp)) l ++
+ str" are implicit" ++ fnl()
+
+let print_impl_args l =
+ if !Options.v7 then print_impl_args_by_pos (positions_of_implicits l)
+ else print_impl_args_by_name (List.filter is_status_implicit l)
let print_argument_scopes = function
| [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
@@ -58,6 +70,10 @@ let print_argument_scopes = function
str "]") ++ fnl()
| _ -> mt()
+let print_name_infos ref =
+ print_impl_args (implicits_of_global ref) ++
+ print_argument_scopes (Symbols.find_arguments_scope ref)
+
(* To be improved; the type should be used to provide the types in the
abstractions. This should be done recursively inside prterm, so that
the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
@@ -163,8 +179,7 @@ let print_mutual sp =
let print_section_variable sp =
let d = get_variable sp in
print_named_decl d ++
- print_impl_args (implicits_of_global (VarRef sp)) ++
- print_argument_scopes (Symbols.find_arguments_scope (VarRef sp))
+ print_name_infos (VarRef sp)
let print_body = function
| Some lc -> prterm (Declarations.force lc)
@@ -187,8 +202,7 @@ let print_constant with_values sep sp =
print_basename sp ++ str sep ++ cut () ++
(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
fnl ()) ++
- print_impl_args (implicits_of_global (ConstRef sp)) ++
- print_argument_scopes (Symbols.find_arguments_scope (ConstRef sp))
+ print_name_infos (ConstRef sp)
let print_inductive sp = (print_mutual sp)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 9326ff538..6b89169b5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -183,6 +183,10 @@ let mlexpr_of_red_flags {
Rawterm.rConst = $mlexpr_of_list mlexpr_of_reference l$
} >>
+let mlexpr_of_explicitation = function
+ | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >>
+ | Topconstr.ExplByPos n -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
+
let rec mlexpr_of_constr = function
| Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
anti loc (string_of_id id)
@@ -195,7 +199,7 @@ let rec mlexpr_of_constr = function
| Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
| Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
- | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
+ | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
| Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index ec1405f76..784c977dd 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -87,12 +87,12 @@ let pr_sort = function
| RProp Term.Pos -> str "Set"
| RType u -> str "Type" ++ pr_opt pr_universe u
-let pr_explicitation = function
- | None -> mt ()
- | Some n -> str "@" ++ int n ++ str ":="
-
let pr_expl_args pr (a,expl) =
- pr_explicitation expl ++ pr (lapp,L) a
+ match expl with
+ | None -> pr (lapp,L) a
+ | Some (_,ExplByPos n) -> str "@" ++ int n ++ str ":=" ++ pr (lapp,L) a
+ | Some (_,ExplByName id) ->
+ str "(" ++ pr_id id ++ str ":=" ++ pr (lapp,L) a ++ str ")"
let pr_opt_type pr = function
| CHole _ -> mt ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:57:09 +0000