diff options
| author | herbelin | 2002-04-10 16:07:52 +0000 |
|---|---|---|
| committer | herbelin | 2002-04-10 16:07:52 +0000 |
| commit | 9b8e006e0c84408992f42bd9d713eacf2936a6d3 (patch) | |
| tree | 890f9572f385abe4dd80506ee2bb0c0ac81392b9 /contrib | |
| parent | d69ce3d0733a7e306514734a2b56d7e112f84f1d (diff) | |
Amélioration des messages d'erreurs concernant l'inférence des implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/pcic.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index ab8eab6c9e..e6f6891f73 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -134,14 +134,14 @@ let tuple_ref dep n = (* Binders. *) -let trad_binder avoid nenv = function - | CC_untyped_binder -> RHole None +let trad_binder avoid nenv id = function + | CC_untyped_binder -> RHole (dummy_loc,AbstractionType (Name id)) | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty let rec push_vars avoid nenv = function | [] -> ([],avoid,nenv) | (id,b) :: bl -> - let b' = trad_binder avoid nenv b in + let b' = trad_binder avoid nenv id b in let bl',avoid',nenv' = push_vars (id :: avoid) (add_name (Name id) nenv) bl in @@ -200,7 +200,9 @@ let rawconstr_of_prog p = | CC_tuple (false,_,[e1;e2]) -> let c1 = trad avoid nenv e1 and c2 = trad avoid nenv e2 in - RApp (dummy_loc, RRef (dummy_loc,pair), [RHole None;RHole None;c1;c2]) + RApp (dummy_loc, RRef (dummy_loc,pair), + [RHole (dummy_loc,ImplicitArg (pair,1)); + RHole (dummy_loc,ImplicitArg (pair,2));c1;c2]) | CC_tuple (dep,tyl,l) -> let n = List.length l in @@ -220,7 +222,7 @@ let rawconstr_of_prog p = Detyping.detype (Global.env()) avoid nenv c | CC_hole c -> - RCast (dummy_loc, RHole None, + RCast (dummy_loc, RHole (dummy_loc, QuestionMark), Detyping.detype (Global.env()) avoid nenv c) in |