- Fix printing and parsing of primitive projections, including the Set

Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).

1 files changed, 18 insertions, 5 deletions

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index e23a4e4408..15053505e2 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -209,7 +209,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
           sorec stk env subst (PApp(h,Array.append a1 a2)) t
 
       | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
-          let p = Array.length args2 - Array.length args1 in
+         (let p = Array.length args2 - Array.length args1 in
           if p >= 0 then
             let args21, args22 = Array.chop p args2 in
 	    let c = mkApp(c2,args21) in
@@ -218,11 +218,18 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
               | None -> subst
               | Some n -> merge_binding allow_bound_rels stk n c subst in
             Array.fold_left2 (sorec stk env) subst args1 args22
-          else raise PatternMatchingFailure
+          else (* Might be a projection on the right *)
+	    match kind_of_term c2 with
+	    | Proj _ -> 
+	      let subst = sorec stk env subst (PApp (PMeta meta, [|args1.(0)|])) c2 in
+		Array.fold_left2 (sorec stk env) subst (Array.tl args1) args2
+	    | _ -> raise PatternMatchingFailure)
 
       | PApp (c1,arg1), App (c2,arg2) ->
+	let diff = Array.length arg2 - Array.length arg1 in
 	(match c1, kind_of_term c2 with
-	| PRef (ConstRef r), Proj (p,c) ->
+	  (* eta-expanded version of projection against projection *)
+	| PRef (ConstRef r), Proj (p,c) when eq_constant r p ->
       	  let pb = Environ.lookup_projection p env in
 	  let npars = pb.Declarations.proj_npars in
 	  let narg1 = Array.length arg1 in
@@ -232,9 +239,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 		try Array.fold_left2 (sorec stk env) subst args arg2
 		with Invalid_argument _ -> raise PatternMatchingFailure
 	    else raise PatternMatchingFailure
+         (* meta against projection *)
+	| PMeta meta, Proj (p,c) when diff != 0 -> 
+          if diff == -1 then (* One more arg for the meta *)
+	    Array.fold_left2 (sorec stk env) (sorec stk env subst (PApp (c1, [|arg1.(0)|])) c2)
+	      (Array.tl arg1) arg2
+	  else raise PatternMatchingFailure
 	| _ ->
-          (try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
-           with Invalid_argument _ -> raise PatternMatchingFailure))
+          try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
+          with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PApp (PMeta (Some n), [|c1|]), Proj (p2, c2) ->
       	  let ty = Retyping.get_type_of env sigma c2 in