From 184550121303fe264150996f74d64dc7a149099f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 Sep 2003 18:41:39 +0000
Subject: Parsing correct des explicites en cas de projection

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4411 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b4edaaf1ec..c07522cc70 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -524,6 +524,11 @@ let internalise sigma env allow_soapp lvar c =
 	check_projection isproj (List.length args) f;
 	RApp (loc, f, intern_args env args_scopes args)
     | CApp (loc, (isproj,f), args) ->
+        let isproj,f,args = match f with
+          (* Compact notations like "t.(f args') args" *)
+          | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
+          (* Don't compact "(f args') args" to resolve implicits separately *)
+          | _ -> isproj,f,args in
 	let (c, impargs, args_scopes) =
 	  match f with
 	    | CRef ref -> intern_reference env lvar ref
@@ -532,6 +537,7 @@ let internalise sigma env allow_soapp lvar c =
 	let args = intern_impargs c env impargs args_scopes args in
 	check_projection isproj (List.length args) c;
 	(match c with 
+          (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CCases (loc, (po,rtnpo), tms, eqns) ->
-- 
cgit v1.2.3