diff options
| author | herbelin | 2003-08-11 10:25:04 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-11 10:25:04 +0000 |
| commit | ead31bf3e2fe220d02dec59dce66471cc2c66fce (patch) | |
| tree | f2dc8aa43dda43200654e8e28a7556f7b84ae200 /contrib/correctness | |
| parent | aad98c46631f3acb3c71ff7a7f6ae9887627baa8 (diff) | |
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
Diffstat (limited to 'contrib/correctness')
| -rw-r--r-- | contrib/correctness/pcic.ml | 4 | ||||
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index 66ac7b97e9..7394a41c5d 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -180,7 +180,7 @@ let rawconstr_of_prog p = let (bl',avoid',nenv') = push_vars avoid nenv bl in let c1 = trad avoid nenv e1 and c2 = trad avoid' nenv' e2 in - ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |]) + ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None) | CC_lam (bl,e) -> let bl',avoid',nenv' = push_vars avoid nenv bl in @@ -214,7 +214,7 @@ let rawconstr_of_prog p = let c = trad avoid nenv b in let cl = List.map (trad avoid nenv) el in let ty = Detyping.detype (Global.env()) avoid nenv ty in - ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl) + ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None) | CC_expr c -> Detyping.detype (Global.env()) avoid nenv c diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 0e6b3b7d2f..2e3fcac411 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, (false,mk_ref loc1 f), List.map (fun a -> a,None) args) + CApp (join_loc loc1 loc2, (None,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, (false,f), args) + CApp (dummy_loc, (None,f), args) | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" |