Commit c8684a1e authored by Heiko Becker's avatar Heiko Becker

Cleanup for regression test

parent 7f40393f
DIGEST 14eb2e5e017990f6a3f1ccef9be1fc57
Fcertificate_AdditionSimple
R15:39 Flover.CertificateChecker <> <> lib
def 53:55 <> C12
R58:60 Flover.Expressions <> exp ind
R62:62 Coq.QArith.QArith_base <> Q rec
R67:71 Flover.Expressions <> Const constr
R84:84 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R73:75 Flover.Infra.MachineType <> M64 constr
def 102:103 <> u0
R106:108 Flover.Expressions <> exp ind
R110:110 Coq.QArith.QArith_base <> Q rec
R115:117 Flover.Expressions <> Var constr
R119:119 Coq.QArith.QArith_base <> Q rec
def 135:136 <> e3
R139:141 Flover.Expressions <> exp ind
R143:143 Coq.QArith.QArith_base <> Q rec
R148:152 Flover.Expressions <> Binop constr
R163:164 certificate_AdditionSimple <> u0 def
R159:161 certificate_AdditionSimple <> C12 def
R154:157 Flover.Expressions <> Plus constr
def 178:182 <> Rete3
R187:189 Flover.Commands <> Ret constr
R191:192 certificate_AdditionSimple <> e3 def
def 208:229 <> defVars_additionSimple
R236:239 Coq.Init.Logic <> :type_scope:x_'->'_x not
R240:245 Coq.Init.Datatypes <> option ind
R247:251 Flover.Infra.MachineType <> mType ind
R233:235 Coq.Init.Datatypes <> nat ind
R270:273 Coq.Arith.PeanoNat <> :nat_scope:x_'=?'_x not
R269:269 certificate_AdditionSimple <> n var
R295:298 Coq.Init.Datatypes <> None constr
R281:284 Coq.Init.Datatypes <> Some constr
R286:288 Flover.Infra.MachineType <> M64 constr
def 312:341 <> thePrecondition_additionSimple
R343:349 Flover.Infra.Abbrevs <> precond def
R361:363 Coq.Init.Datatypes <> nat ind
R373:376 Coq.Arith.PeanoNat <> :nat_scope:x_'=?'_x not
R372:372 certificate_AdditionSimple <> n var
R414:414 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R418:418 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R422:422 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R416:416 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R420:420 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R384:385 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R396:397 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R407:407 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R386:386 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R391:392 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R403:403 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
def 437:457 <> absenv_additionSimple
R460:473 Flover.Infra.ExpressionAbbrevs <> analysisResult def
R494:506 Flover.Infra.ExpressionAbbrevs FloverMap add def
R598:610 Flover.Infra.ExpressionAbbrevs FloverMap add def
R668:680 Flover.Infra.ExpressionAbbrevs FloverMap add def
R743:757 Flover.Infra.ExpressionAbbrevs FloverMap empty def
R764:766 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
R760:763 Flover.Infra.Abbrevs <> intv def
R767:771 Flover.Infra.Abbrevs <> error def
R686:686 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R712:713 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R740:740 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R687:688 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R699:700 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R711:711 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R695:695 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R707:707 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R720:720 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R682:684 certificate_AdditionSimple <> C12 def
R615:615 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R640:641 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R665:665 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R616:617 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R628:629 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R639:639 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R618:618 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R623:624 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R635:635 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R646:646 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R612:613 certificate_AdditionSimple <> u0 def
R511:511 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R537:538 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R595:595 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R512:513 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R524:525 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R536:536 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R520:520 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R532:532 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R560:560 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R508:509 certificate_AdditionSimple <> e3 def
prf 787:817 <> ErrorBound_additionSimple_Sound
R924:926 Coq.Init.Logic <> :type_scope:x_'='_x not
R821:841 Flover.CertificateChecker <> CertificateCheckerCmd def
R902:923 certificate_AdditionSimple <> defVars_additionSimple def
R871:900 certificate_AdditionSimple <> thePrecondition_additionSimple def
R849:869 certificate_AdditionSimple <> absenv_additionSimple def
R843:847 certificate_AdditionSimple <> Rete3 def
R927:930 Coq.Init.Datatypes <> true constr
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment