diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-10 21:02:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-10 21:02:46 +0000 |
| commit | 2f562f15a72d4a379d559ea1987e74c1c24d1391 (patch) | |
| tree | 3bbec40fab01fa5af88b88e83297a5cfd7ae2804 /contrib/interface | |
| parent | a3595484aadf71296f2d5af85b9eb0a3c74a3526 (diff) | |
Ajout notation c.(f) en v8 pour les projections de Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/pbp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 74ecdaaa3..487f45057 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -144,7 +144,7 @@ let (imply_intro1: pbp_rule) = function let make_var id = CRef (Ident(zz, id)) -let make_app f l = CApp (zz,f,List.map (fun x -> (x,None)) l) +let make_app f l = CApp (zz,(false,f),List.map (fun x -> (x,None)) l) let make_pbp_pattern x = make_app (make_var (id_of_string "PBP_META")) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b83ce2d71..14caa9f98 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -308,10 +308,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b) | CLetIn(_, v, a, b) -> CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b) - | CAppExpl(_, r, l) -> + | CAppExpl(_, (_,r), l) -> (* TODO: proj notation *) CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)), xlate_formula_ne_list l) - | CApp(_, f, l) -> + | CApp(_, (_,f), l) -> (* TODO: proj notation *) CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) | CCases (_,po,tml,eqns)-> CT_cases(xlate_formula_opt po, xlate_formula_ne_list tml, |