Changeset 882 for src/common


Ignore:
Timestamp:
Jun 3, 2011, 5:35:32 PM (10 years ago)
Author:
campbell
Message:

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r881 r882  
    213213}.
    214214
    215 (*
     215
    216216definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    217217  map ?? (fst ident F) (prog_funct ?? p).
     
    479479  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
    480480Qed.
    481 *)*)
     481*)
    482482(* * * External functions *)
    483483
Note: See TracChangeset for help on using the changeset viewer.