aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml52
-rw-r--r--interp/topconstr.ml2
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--test-suite/output/Notations2.out2
-rw-r--r--test-suite/output/Notations2.v5
-rw-r--r--theories/Init/Logic.v4
6 files changed, 45 insertions, 28 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 389093127..d4639987a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -421,12 +421,12 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
| LocalRawAssum(nal,bk,ty) ->
(match bk with
| Default k ->
- 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
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
List.fold_left
- (fun (env,bl) na ->
- (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+ (fun (env,bl) (loc,na as locna) ->
+ (push_name_env lvar impls env locna,
+ (na,k,None,locate_if_isevar loc na ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -465,12 +465,12 @@ let iterate_binder intern lvar (env,bl) = function
let intern_type env = intern (set_type_scope env) in
(match bk with
| Default k ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
let ty = intern_type env ty in
- let ty = locate_if_isevar loc na ty in
+ let impls = impls_type_list ty in
List.fold_left
- (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+ (fun (env,bl) (loc,na as locna) ->
+ (push_name_env lvar impls env locna,
+ (na,k,None,locate_if_isevar loc na ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -1614,13 +1614,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
(tm',(snd na,typ)), extra_id, match_td
and iterate_prod loc2 env bk ty body nal =
- let rec default env bk = function
- | (loc1,na as locna)::nal ->
- if nal <> [] then check_capture loc1 ty na;
- let ty = locate_if_isevar loc1 na (intern_type env ty) in
- let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
- GProd (join_loc loc1 loc2, na, bk, ty, body)
- | [] -> intern_type env body
+ let default env bk = function
+ | (loc1,na)::nal' as nal ->
+ if nal' <> [] then check_capture loc1 ty na;
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
+ let env = List.fold_left (push_name_env lvar impls) env nal in
+ List.fold_right (fun (loc,na) c ->
+ GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+ nal (intern_type env body)
+ | [] -> assert false
in
match bk with
| Default b -> default env b nal
@@ -1630,13 +1633,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
it_mkGProd ibind body
and iterate_lam loc2 env bk ty body nal =
- let rec default env bk = function
- | (loc1,na as locna)::nal ->
- if nal <> [] then check_capture loc1 ty na;
- let ty = locate_if_isevar loc1 na (intern_type env ty) in
- let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
- GLambda (join_loc loc1 loc2, na, bk, ty, body)
- | [] -> intern env body
+ let default env bk = function
+ | (loc1,na)::nal' as nal ->
+ if nal' <> [] then check_capture loc1 ty na;
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
+ let env = List.fold_left (push_name_env lvar impls) env nal in
+ List.fold_right (fun (loc,na) c ->
+ GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+ nal (intern env body)
+ | [] -> assert false
in match bk with
| Default b -> default env b nal
| Generalized (b, b', t) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8db5b0afa..7d3acf66a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -240,7 +240,7 @@ let compare_recursive_parts found f (iterator,subc) =
| GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
| GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
(* We found a binding position where it differs *)
- check_is_hole y t_x;
+ check_is_hole x t_x;
check_is_hole y t_y;
!diff = None && (diff := Some (x,y,None); aux c term)
| _ ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a8adfb19a..f60d06857 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,6 +31,11 @@ let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
+let binders_of_names l =
+ List.map (fun (loc, na) ->
+ LocalRawAssum ([loc, na], Default Explicit,
+ CHole (loc, Some (Evd.BinderType na)))) l
+
let binders_of_lidents l =
List.map (fun (loc, id) ->
LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
@@ -384,8 +389,7 @@ GEXTEND Gram
[LocalRawAssum (id::idl,Default Explicit,c)]
(* binders factorized with open binder *)
| id = name; idl = LIST0 name; bl = binders ->
- let t = CHole (loc, Some (Evd.BinderType (snd id))) in
- LocalRawAssum (id::idl,Default Explicit,t)::bl
+ binders_of_names (id::idl) @ bl
| id1 = name; ".."; id2 = name ->
[LocalRawAssum ([id1;(loc,Name ldots_var);id2],
Default Explicit,CHole (loc,None))]
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 3b3351d33..cf45025ea 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,6 +10,8 @@ end
: nat
let '(a, _, _) := (2, 3, 4) in a
: nat
+exists myx (y : bool), myx = y
+ : Prop
fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
: (nat -> nat -> Prop) -> nat -> Prop
∃ n p : nat, n + p = 0
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 1fcbe858a..e53c94ef0 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -25,6 +25,11 @@ Remove Printing Let prod.
Check match (0,0,0) with (x,y,z) => x+y+z end.
Check let '(a,b,c) := ((2,3),4) in a.
+(* Check printing of notations with mixed reserved binders (see bug #2571) *)
+
+Implicit Type myx : bool.
+Check exists myx y, myx = y.
+
(* Test notation for anonymous functions up to eta-expansion *)
Check fun P:nat->nat->Prop => fun x:nat => ex (P x).
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d8a028cfb..ca7d0073e 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -240,7 +240,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
(at level 200, x binder, right associativity,
- format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
+ format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
@@ -423,7 +423,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
Notation "'exists' ! x .. y , p" :=
(ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
(at level 200, x binder, right associativity,
- format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'")
+ format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'")
: type_scope.
Lemma unique_existence : forall (A:Type) (P:A->Prop),
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 17:31:55 +0000