Ignore:
Timestamp:
Feb 25, 2013, 6:43:44 PM (7 years ago)
Author:
campbell
Message:

Remove a couple of redundant hypotheses.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2726 r2727  
    288288          destruct >Etrace
    289289          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    290           [1,3: whd in match (cs_classify ??); >CL %
    291           |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     290          [ whd in match (cs_classify ??); >CL %
     291          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    292292          | @INV
    293293          | assumption
     
    533533          destruct >Etrace
    534534          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    535           [1,3: whd in match (cs_classify ??); >CL %
    536           |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     535          [ whd in match (cs_classify ??); >CL %
     536          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    537537          | @INV
    538538          | assumption
Note: See TracChangeset for help on using the changeset viewer.