aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml10
-rw-r--r--interp/constrintern.ml95
-rw-r--r--interp/constrintern.mli6
-rw-r--r--interp/dumpglob.ml7
-rw-r--r--interp/dumpglob.mli1
-rw-r--r--interp/topconstr.ml23
-rw-r--r--interp/topconstr.mli6
-rw-r--r--lib/util.ml6
-rw-r--r--lib/util.mli6
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--parsing/ppconstr.ml6
-rw-r--r--toplevel/command.ml5
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml1
14 files changed, 90 insertions, 92 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 28cd12fbd..95a669f75 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -684,10 +684,10 @@ let rec extern inctx scopes vars r =
let na' = match na,tm with
Anonymous, RVar (_,id) when
rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
- -> Some Anonymous
+ -> Some (dummy_loc,Anonymous)
| Anonymous, _ -> None
| Name id, RVar (_,id') when id=id' -> None
- | Name _, _ -> Some na in
+ | Name _, _ -> Some (dummy_loc,na) in
(sub_extern false scopes vars tm,
(na',Option.map (fun (loc,ind,n,nal) ->
let params = list_tabulate
@@ -701,15 +701,15 @@ let rec extern inctx scopes vars r =
CCases (loc,sty,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
- CLetTuple (loc,nal,
- (Option.map (fun _ -> na) typopt,
+ CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
+ (Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
- (Option.map (fun _ -> na) typopt,
+ (Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bc5cdf726..81ddb2731 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -288,24 +288,19 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
-let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
- | Anonymous ->
- if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
+let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
+ function
+ | loc,Anonymous ->
+ if global_level then
+ user_err_loc (loc,"", str "Anonymous variables not allowed");
env
- | Name id ->
+ | loc,Name id ->
check_hidden_implicit_parameters id lvar;
- (Idset.add id ids, unb,tmpsc,scopes)
-
-let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
- | Anonymous ->
- if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
- env
- | Name id ->
- check_hidden_implicit_parameters id lvar;
- Dumpglob.dump_binding loc id;
+ if global_level then Dumpglob.dump_definition (loc,id) true "var"
+ else Dumpglob.dump_binding loc id;
(Idset.add id ids,unb,tmpsc,scopes)
-let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
+let intern_generalized_binder ?(global_level=false) intern_type lvar
(ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in
let ty, ids' =
@@ -315,11 +310,11 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
in
let ty' = intern_type (ids,true,tmpsc,sc) ty in
let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
- let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
+ let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in
let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
let na = match na with
| Anonymous ->
- if fail_anonymous then na
+ if global_level then na
else
let name =
let id =
@@ -329,24 +324,24 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
| _ -> na
- in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
+ in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl
-let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
+let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function
| LocalRawAssum(nal,bk,ty) ->
(match bk with
| Default k ->
- let (loc,na) = List.hd nal in
+ let (loc,na) = (List.hd nal) in
(* TODO: fail if several names with different implicit types *)
let ty = locate_if_isevar loc na (intern_type env ty) in
List.fold_left
- (fun ((ids,unb,ts,sc),bl) (_,na) ->
- ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
+ (fun (env,bl) na ->
+ (push_name_env lvar env na,(snd na,k,None,ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
- let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in
+ let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
env, b @ bl)
- | LocalRawDef((loc,na),def) ->
- ((name_fold Idset.add na ids,unb,ts,sc),
+ | LocalRawDef((loc,na as locna),def) ->
+ (push_name_env lvar env locna,
(na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
@@ -369,7 +364,7 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a
RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
in
List.fold_right (fun (id, loc as lid) (env, acc) ->
- let env' = push_loc_name_env lvar env loc (Name id) in
+ let env' = push_name_env lvar env (loc, Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -1101,9 +1096,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
intern env c2
| CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
- | CLetIn (loc,(loc1,na),c1,c2) ->
- RLetIn (loc, na, intern (reset_tmp_scope env) c1,
- intern (push_loc_name_env lvar env loc1 na) c2)
+ | CLetIn (loc,na,c1,c2) ->
+ RLetIn (loc, snd na, intern (reset_tmp_scope env) c1,
+ intern (push_name_env lvar env na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -1171,7 +1166,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
let p' = Option.map (fun p ->
let env'' = List.fold_left (push_name_env lvar) env ids in
intern_type env'' p) po in
- RLetTuple (loc, nal, (na', p'), b',
+ RLetTuple (loc, List.map snd nal, (na', p'), b',
intern (List.fold_left (push_name_env lvar) env nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
@@ -1246,27 +1241,27 @@ let internalize sigma globalenv env allow_patvar lvar c =
if List.length l <> nindargs then
error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
let nal = List.map (function
- | RHole loc -> Anonymous
- | RVar (_,id) -> Name id
+ | RHole (loc,_) -> loc,Anonymous
+ | RVar (loc,id) -> loc,Name id
| c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
let parnal,realnal = list_chop nparams nal in
- if List.exists ((<>) Anonymous) parnal then
+ if List.exists (fun (_,na) -> na <> Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
- realnal, Some (loc,ind,nparams,realnal)
+ realnal, Some (loc,ind,nparams,List.map snd realnal)
| None ->
[], None in
let na = match tm', na with
- | RVar (_,id), None when Idset.mem id vars -> Name id
- | RRef (loc, VarRef id), None -> Name id
- | _, None -> Anonymous
- | _, Some na -> na in
- (tm',(na,typ)), na::ids
+ | RVar (loc,id), None when Idset.mem id vars -> loc,Name id
+ | RRef (loc, VarRef id), None -> loc,Name id
+ | _, None -> dummy_loc,Anonymous
+ | _, Some (loc,na) -> loc,na in
+ (tm',(snd na,typ)), na::ids
and iterate_prod loc2 env bk ty body nal =
let rec default env bk = function
- | (loc1,na)::nal ->
+ | (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+ let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
RProd (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern_type env body
@@ -1281,9 +1276,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
and iterate_lam loc2 env bk ty body nal =
let rec default env bk = function
- | (loc1,na)::nal ->
+ | (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+ let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
RLambda (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern env body
@@ -1488,10 +1483,10 @@ let my_intern_constr sigma env lvar acc c =
let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-let intern_context fail_anonymous sigma env params =
+let intern_context global_level sigma env params =
let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
snd (List.fold_left
- (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
+ (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
((extract_ids env,false,None,[]), []) params)
let interp_rawcontext_gen understand_type understand_judgment env bl =
@@ -1517,15 +1512,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params =
- let bl = intern_context fail_anonymous sigma env params in
+let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params =
+ let bl = intern_context global_level sigma env params in
interp_rawcontext_gen understand_type understand_judgment env bl
-let interp_context ?(fail_anonymous=false) sigma env params =
+let interp_context ?(global_level=false) sigma env params =
interp_context_gen (Default.understand_type sigma)
- (Default.understand_judgment sigma) ~fail_anonymous sigma env params
+ (Default.understand_judgment sigma) ~global_level sigma env params
-let interp_context_evars ?(fail_anonymous=false) evdref env params =
+let interp_context_evars ?(global_level=false) evdref env params =
interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
- (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params
+ (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 326089d37..1dd221f69 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -155,13 +155,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
val interp_context_gen : (env -> rawconstr -> types) ->
(env -> rawconstr -> unsafe_judgment) ->
- ?fail_anonymous:bool ->
+ ?global_level:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context : ?fail_anonymous:bool ->
+val interp_context : ?global_level:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context_evars : ?fail_anonymous:bool ->
+val interp_context_evars : ?global_level:bool ->
evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(** Locating references of constructions, possibly via a syntactic definition
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 9dfa808c7..59d1abb8e 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -159,13 +159,6 @@ let dump_name (loc, n) sec ty =
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
-let dump_local_binder b sec ty =
- if dump () then
- match b with
- | Topconstr.LocalRawAssum (nl, _, _) ->
- List.iter (fun x -> dump_name x sec ty) nl
- | Topconstr.LocalRawDef _ -> ()
-
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 023608490..5484a6360 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -36,7 +36,6 @@ val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation
val dump_binding : Util.loc -> Names.Idset.elt -> unit
val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit
-val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0aa4339dd..db6de8fd1 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -699,11 +699,11 @@ type constr_expr =
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
- (constr_expr * (name option * constr_expr option)) list *
+ (constr_expr * (name located option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
- | CLetTuple of loc * name list * (name option * constr_expr option) *
+ | CLetTuple of loc * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
- | CIf of loc * constr_expr * (name option * constr_expr option)
+ | CIf of loc * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
@@ -807,7 +807,7 @@ let ids_of_cases_tomatch tms =
List.fold_right
(fun (_,(ona,indnal)) l ->
Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
- indnal (Option.fold_right name_cons ona l))
+ indnal (Option.fold_right (down_located name_cons) ona l))
tms []
let is_constructor id =
@@ -872,11 +872,12 @@ let fold_constr_expr_with_binders g f n acc = function
let ids = ids_of_pattern_list patl in
f (Idset.fold g ids n) acc rhs) bl acc
| CLetTuple (loc,nal,(ona,po),b,c) ->
- let n' = List.fold_right (name_fold g) nal n in
- f (Option.fold_right (name_fold g) ona n') (f n acc b) c
+ let n' = List.fold_right (down_located (name_fold g)) nal n in
+ f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
| CIf (_,c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
- Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
+ Option.fold_left
+ (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
| CFix (loc,_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -981,7 +982,7 @@ let split_at_annot bl na =
(* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
+let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -1025,11 +1026,11 @@ let map_constr_expr_with_binders g f e = function
let po = Option.map (f (List.fold_right g ids e)) rtnpo in
CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
- let e' = List.fold_right (name_fold g) nal e in
- let e'' = Option.fold_right (name_fold g) ona e in
+ let e' = List.fold_right (down_located (name_fold g)) nal e in
+ let e'' = Option.fold_right (down_located (name_fold g)) ona e in
CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (loc,c,(ona,po),b1,b2) ->
- let e' = Option.fold_right (name_fold g) ona e in
+ let e' = Option.fold_right (down_located (name_fold g)) ona e in
CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3a50475db..5ce488b9a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -133,11 +133,11 @@ type constr_expr =
(constr_expr * explicitation located option) list
| CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
- (constr_expr * (name option * constr_expr option)) list *
+ (constr_expr * (name located option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
- | CLetTuple of loc * name list * (name option * constr_expr option) *
+ | CLetTuple of loc * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
- | CIf of loc * constr_expr * (name option * constr_expr option)
+ | CIf of loc * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
diff --git a/lib/util.ml b/lib/util.ml
index 20481adf3..16e00a089 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -42,6 +42,7 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
@@ -65,6 +66,11 @@ let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a
+(* Projection operator *)
+
+let down_fst f x = f (fst x)
+let down_snd f x = f (snd x)
+
(* Characters *)
let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
diff --git a/lib/util.mli b/lib/util.mli
index bbef3462a..e5b6cd544 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -51,6 +51,7 @@ val user_err_loc : loc * string * std_ppcmds -> 'a
val invalid_arg_loc : loc * string -> 'a
val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+val down_located : ('a -> 'b) -> 'a located -> 'b
(** Like [Exc_located], but specifies the outermost file read, the
input buffer associated to the location of the error (or the module name
@@ -63,6 +64,11 @@ exception Error_in_file of string * (bool * string * loc) * exn
val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+(** Going down pairs *)
+
+val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
+val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
+
(** Mapping under triple *)
val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 087ae31ae..e3c898284 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -124,7 +124,7 @@ let ident_with =
| _ -> err ())
| _ -> err ())
-let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
+let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
@@ -251,7 +251,7 @@ GEXTEND Gram
po = return_type;
":="; c1 = operconstr LEVEL "200"; "in";
c2 = operconstr LEVEL "200" ->
- CLetTuple (loc,List.map snd lb,po,c1,c2)
+ CLetTuple (loc,lb,po,c1,c2)
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
@@ -308,14 +308,14 @@ GEXTEND Gram
[ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
;
pred_pattern:
- [ [ ona = OPT ["as"; id=name -> snd id];
+ [ [ ona = OPT ["as"; id=name -> id];
ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ]
;
case_type:
[ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
;
return_type:
- [ [ a = OPT [ na = OPT["as"; id=name -> snd id];
+ [ [ a = OPT [ na = OPT["as"; na=name -> na];
ty = case_type -> (na,ty) ] ->
match a with
| None -> None, None
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 2d63b20bb..6a4d9757d 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -365,7 +365,7 @@ let tm_clash = function
let pr_asin pr (na,indnalopt) =
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
- | Some na -> spc () ++ str "as " ++ pr_name na
+ | Some na -> spc () ++ str "as " ++ pr_lname na
| None -> mt ()) ++
(match indnalopt with
| None -> mt ()
@@ -384,7 +384,7 @@ let pr_return_type pr po = pr_case_type pr po
let pr_simple_return_type pr na po =
(match na with
- | Some (Name id) ->
+ | Some (_,Name id) ->
spc () ++ str "as " ++ pr_id id
| _ -> mt ()) ++
pr_case_type pr po
@@ -518,7 +518,7 @@ let pr pr sep inherited a =
hv 0 (
str "let " ++
hov 0 (str "(" ++
- prlist_with_sep sep_v pr_name nal ++
+ prlist_with_sep sep_v pr_lname nal ++
str ")" ++
pr_simple_return_type (pr mt) na po ++ str " :=" ++
pr spc ltop c ++ str " in") ++
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3fa83662b..a16afa86c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -67,8 +67,7 @@ let red_constant_entry n ce = function
let interp_definition boxed bl red_option c ctypopt =
let env = Global.env() in
let evdref = ref Evd.empty in
- let (env_bl, ctx), imps1 =
- interp_context_evars ~fail_anonymous:false evdref env bl in
+ let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
let imps,ce =
match ctypopt with
None ->
@@ -225,7 +224,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
let env0 = Global.env() in
let evdref = ref Evd.empty in
let (env_params, ctx_params), userimpls =
- interp_context_evars ~fail_anonymous:false evdref env0 paramsl
+ interp_context_evars evdref env0 paramsl
in
let indnames = List.map (fun ind -> ind.ind_name) indl in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 89bf76911..12843da60 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -60,7 +60,7 @@ let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields id t ps nots fs =
let env0 = Global.env () in
let evars = ref Evd.empty in
- let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
+ let (env1,newps), imps = interp_context_evars evars env0 ps in
let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0ed1186a0..6a1eff333 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -599,7 +599,6 @@ let vernac_instance abst glob sup inst props pri =
ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
let vernac_context l =
- List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
Classes.context l
let vernac_declare_instance glob id =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 01:44:59 +0000