diff options
| author | herbelin | 2003-06-10 21:20:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-06-10 21:20:34 +0000 |
| commit | 11a923b21b669d1a8e1c51afd42caf38d20fb79d (patch) | |
| tree | 36c9206c6bb1f57feda8ed6d2ecfe481df502e83 /contrib | |
| parent | 610869d3db9f101718d39a4530ab7b84e4c054c2 (diff) | |
Ajout notation c.(f) en v8 pour les projections de Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 888f876dee..0e6b3b7d2f 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -107,7 +107,7 @@ open Coqast let mk_id loc id = mkRefC (Ident (loc, id)) let mk_ref loc s = mk_id loc (id_of_string s) let mk_appl loc1 loc2 f args = - CApp (join_loc loc1 loc2, mk_ref loc1 f, List.map (fun a -> a,None) args) + CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args) let conj_assert {a_name=n;a_value=a} {a_value=b} = let loc1 = constr_loc a in @@ -166,7 +166,7 @@ let rec coqast_of_program loc = function (function Term t -> (coqast_of_program t.loc t.desc,None) | _ -> invalid_arg "coqast_of_program") l in - CApp (dummy_loc, f, args) + CApp (dummy_loc, (false,f), args) | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" |