Changeset 1045 for src/common


Ignore:
Timestamp:
Jun 29, 2011, 10:47:39 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict in rtlabs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r985 r1045  
    6969#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
    7070try ( @Ptrue // )
    71 @Pfalse % #E destruct;
     71@Pfalse % #E destruct
    7272qed.
    7373
     
    274274
    275275definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    276   map ?? (fst ident F) (prog_funct ?? p).
     276  map ? ? (fst ident F) (prog_funct ?? p).
    277277
    278278definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
     
    594594
    595595
    596 
    597596(* Partially merged stuff derived from the prototype cerco compiler. *)
    598597
     598(*
    599599definition bool_to_Prop ≝
    600600 λb. match b with [ true ⇒ True | false ⇒ False ].
    601601
    602602coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     603*)
    603604
    604605(* dpm: should go to standard library *)
Note: See TracChangeset for help on using the changeset viewer.