diff options
| -rwxr-xr-x | theories/Init/Logic.v | 5 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 18 |
2 files changed, 15 insertions, 8 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4c284818b..dc067a4b7 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -78,7 +78,7 @@ Theorem iff_refl : (A:Prop) (iff A A). Split; Auto. Qed. -Theorem iff_trans : (A,B,C:Prop) (iff A B) -> (iff B C) -> (iff A C). +Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c). Proof. Intros A B C (H1,H2) (H3,H4); Split; Auto. Qed. @@ -92,7 +92,8 @@ End Equivalence. (** [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)], denotes either [P] and [Q], or [~P] and [Q] *) -Definition IF := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). +Definition IF_then_else := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). +V7only [Notation IF:=IF_then_else.]. Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (at level 1, c1, c2, c3 at level 8) : type_scope diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 33d6ce786..2b37b945b 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -729,21 +729,26 @@ let is_arith ref = let sp = sp_of_global ref in is_arith_dir (dirpath sp) (basename sp) -let get_name (ln,lp,lz) id n = +let get_name (ln,lp,lz,ll) id n = let id' = string_of_id n in (match id' with - | "nat" -> (id_of_string (List.hd ln),(List.tl ln,lp,lz)) - | "positive" -> (id_of_string (List.hd lp),(ln,List.tl lp,lz)) - | "Z" -> (id_of_string (List.hd lz),(ln,lp,List.tl lz)) - | _ -> id,(ln,lp,lz)) + | "nat" -> (id_of_string (List.hd ln),(List.tl ln,lp,lz,ll)) + | "positive" -> (id_of_string (List.hd lp),(ln,List.tl lp,lz,ll)) + | "Z" -> (id_of_string (List.hd lz),(ln,lp,List.tl lz,ll)) + | "Prop" when List.mem (string_of_id id) ["a";"b";"c"] -> + (* pour iff_trans *) + (id_of_string (List.hd ll),(ln,lp,lz,List.tl ll)) + | _ -> id,(ln,lp,lz,ll)) let get_name_constr names id t = match kind_of_term t with | Ind ind -> let n = basename (sp_of_global (IndRef ind)) in get_name names id n + | Sort _ -> get_name names id (id_of_string "Prop") | _ -> id,names -let names = (["n";"m";"p";"q"],["p";"q";"r";"s"],["n";"m";"p";"q"]) +let names = + (["n";"m";"p";"q"],["p";"q";"r";"s"],["n";"m";"p";"q"],["A";"B";"C"]) let znames t = let rec aux c names = match kind_of_term c with @@ -757,6 +762,7 @@ let znames t = let get_name_raw names id t = match t with | CRef(Ident (_,n)) -> get_name names id n + | CSort _ -> get_name names id (id_of_string "Prop") | _ -> id,names let rename_bound_variables id t = |