From ead31bf3e2fe220d02dec59dce66471cc2c66fce Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 11 Aug 2003 10:25:04 +0000 Subject: Nouvelle mouture du traducteur v7->v8 Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/pbp.ml | 2 +- contrib/interface/xlate.ml | 9 ++++++--- 2 files changed, 7 insertions(+), 4 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 487f45057c..3d01dd92fe 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,(false,f),List.map (fun x -> (x,None)) l) +let make_app f l = CApp (zz,(None,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 c0ba10bddf..8d82da7e1f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -313,14 +313,17 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function xlate_formula_ne_list 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, + | CCases (_,(po,None),tml,eqns)-> CT_cases(xlate_formula_opt po, + xlate_formula_ne_list (List.map fst tml), CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns)) + | CCases (_,(po,Some _),tml,eqns)-> xlate_error "TODO" | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> CT_if(xlate_formula_opt po, xlate_formula c,xlate_formula b1,xlate_formula b2) + | CLetTuple (_,l, (na,po), c, b) -> xlate_error "LetTuple: TODO" + | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) -> CT_inductive_let(xlate_formula_opt po, xlate_id_opt_ne_list l, @@ -1500,7 +1503,7 @@ let xlate_vernac = | (*Record from tactics/Record.v *) VernacRecord - ((add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) -> + (_, (add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) -> let record_constructor = xlate_ident_opt rec_constructor_or_none in CT_record ((if add_coercion then CT_coercion_atm else -- cgit v1.2.3