diff options
Diffstat (limited to 'src/Trace.v')
| -rw-r--r-- | src/Trace.v | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/src/Trace.v b/src/Trace.v index 3f61dc7..85671f9 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -778,6 +778,127 @@ End Euf_Checker. Unset Implicit Arguments. +(* Register constants for OCaml access *) +Register Sat_Checker.valid as SMTCoq.Trace.Sat_Checker.valid. +Register Sat_Checker.interp_var as SMTCoq.Trace.Sat_Checker.interp_var. +Register Sat_Checker.Certif as SMTCoq.Trace.Sat_Checker.Certif. +Register Sat_Checker.step as SMTCoq.Trace.Sat_Checker.step. +Register Sat_Checker.Res as SMTCoq.Trace.Sat_Checker.Res. +Register Sat_Checker.dimacs as SMTCoq.Trace.Sat_Checker.dimacs. +Register Sat_Checker.certif as SMTCoq.Trace.Sat_Checker.certif. +Register Sat_Checker.theorem_checker as SMTCoq.Trace.Sat_Checker.theorem_checker. +Register Sat_Checker.checker as SMTCoq.Trace.Sat_Checker.checker. + +Register Cnf_Checker.certif as SMTCoq.Trace.Cnf_Checker.certif. +Register Cnf_Checker.Certif as SMTCoq.Trace.Cnf_Checker.Certif. +Register Cnf_Checker.checker_b_correct as SMTCoq.Trace.Cnf_Checker.checker_b_correct. +Register Cnf_Checker.checker_b as SMTCoq.Trace.Cnf_Checker.checker_b. +Register Cnf_Checker.checker_eq_correct as SMTCoq.Trace.Cnf_Checker.checker_eq_correct. +Register Cnf_Checker.checker_eq as SMTCoq.Trace.Cnf_Checker.checker_eq. +Register Cnf_Checker.step as SMTCoq.Trace.Cnf_Checker.step. +Register Cnf_Checker.Res as SMTCoq.Trace.Cnf_Checker.Res. +Register Cnf_Checker.ImmFlatten as SMTCoq.Trace.Cnf_Checker.ImmFlatten. +Register Cnf_Checker.CTrue as SMTCoq.Trace.Cnf_Checker.CTrue. +Register Cnf_Checker.CFalse as SMTCoq.Trace.Cnf_Checker.CFalse. +Register Cnf_Checker.BuildDef as SMTCoq.Trace.Cnf_Checker.BuildDef. +Register Cnf_Checker.BuildDef2 as SMTCoq.Trace.Cnf_Checker.BuildDef2. +Register Cnf_Checker.BuildProj as SMTCoq.Trace.Cnf_Checker.BuildProj. +Register Cnf_Checker.ImmBuildDef as SMTCoq.Trace.Cnf_Checker.ImmBuildDef. +Register Cnf_Checker.ImmBuildDef2 as SMTCoq.Trace.Cnf_Checker.ImmBuildDef2. +Register Cnf_Checker.ImmBuildProj as SMTCoq.Trace.Cnf_Checker.ImmBuildProj. + +Register Euf_Checker.Certif as SMTCoq.Trace.Euf_Checker.Certif. +Register Euf_Checker.certif as SMTCoq.Trace.Euf_Checker.certif. +Register Euf_Checker.checker as SMTCoq.Trace.Euf_Checker.checker. +Register Euf_Checker.checker_correct as SMTCoq.Trace.Euf_Checker.checker_correct. +Register Euf_Checker.checker_b_correct as SMTCoq.Trace.Euf_Checker.checker_b_correct. +Register Euf_Checker.checker_b as SMTCoq.Trace.Euf_Checker.checker_b. +Register Euf_Checker.checker_eq_correct as SMTCoq.Trace.Euf_Checker.checker_eq_correct. +Register Euf_Checker.checker_eq as SMTCoq.Trace.Euf_Checker.checker_eq. +Register Euf_Checker.checker_debug as SMTCoq.Trace.Euf_Checker.checker_debug. +Register Euf_Checker.name_step as SMTCoq.Trace.Euf_Checker.name_step. +Register Euf_Checker.Name_Res as SMTCoq.Trace.Euf_Checker.Name_Res. +Register Euf_Checker.Name_Weaken as SMTCoq.Trace.Euf_Checker.Name_Weaken. +Register Euf_Checker.Name_ImmFlatten as SMTCoq.Trace.Euf_Checker.Name_ImmFlatten. +Register Euf_Checker.Name_CTrue as SMTCoq.Trace.Euf_Checker.Name_CTrue. +Register Euf_Checker.Name_CFalse as SMTCoq.Trace.Euf_Checker.Name_CFalse. +Register Euf_Checker.Name_BuildDef as SMTCoq.Trace.Euf_Checker.Name_BuildDef. +Register Euf_Checker.Name_BuildDef2 as SMTCoq.Trace.Euf_Checker.Name_BuildDef2. +Register Euf_Checker.Name_BuildProj as SMTCoq.Trace.Euf_Checker.Name_BuildProj. +Register Euf_Checker.Name_ImmBuildDef as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef. +Register Euf_Checker.Name_ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef2. +Register Euf_Checker.Name_ImmBuildProj as SMTCoq.Trace.Euf_Checker.Name_ImmBuildProj. +Register Euf_Checker.Name_EqTr as SMTCoq.Trace.Euf_Checker.Name_EqTr. +Register Euf_Checker.Name_EqCgr as SMTCoq.Trace.Euf_Checker.Name_EqCgr. +Register Euf_Checker.Name_EqCgrP as SMTCoq.Trace.Euf_Checker.Name_EqCgrP. +Register Euf_Checker.Name_LiaMicromega as SMTCoq.Trace.Euf_Checker.Name_LiaMicromega. +Register Euf_Checker.Name_LiaDiseq as SMTCoq.Trace.Euf_Checker.Name_LiaDiseq. +Register Euf_Checker.Name_SplArith as SMTCoq.Trace.Euf_Checker.Name_SplArith. +Register Euf_Checker.Name_SplDistinctElim as SMTCoq.Trace.Euf_Checker.Name_SplDistinctElim. +Register Euf_Checker.Name_BBVar as SMTCoq.Trace.Euf_Checker.Name_BBVar. +Register Euf_Checker.Name_BBConst as SMTCoq.Trace.Euf_Checker.Name_BBConst. +Register Euf_Checker.Name_BBOp as SMTCoq.Trace.Euf_Checker.Name_BBOp. +Register Euf_Checker.Name_BBNot as SMTCoq.Trace.Euf_Checker.Name_BBNot. +Register Euf_Checker.Name_BBNeg as SMTCoq.Trace.Euf_Checker.Name_BBNeg. +Register Euf_Checker.Name_BBAdd as SMTCoq.Trace.Euf_Checker.Name_BBAdd. +Register Euf_Checker.Name_BBConcat as SMTCoq.Trace.Euf_Checker.Name_BBConcat. +Register Euf_Checker.Name_BBMul as SMTCoq.Trace.Euf_Checker.Name_BBMul. +Register Euf_Checker.Name_BBUlt as SMTCoq.Trace.Euf_Checker.Name_BBUlt. +Register Euf_Checker.Name_BBSlt as SMTCoq.Trace.Euf_Checker.Name_BBSlt. +Register Euf_Checker.Name_BBEq as SMTCoq.Trace.Euf_Checker.Name_BBEq. +Register Euf_Checker.Name_BBDiseq as SMTCoq.Trace.Euf_Checker.Name_BBDiseq. +Register Euf_Checker.Name_BBExtract as SMTCoq.Trace.Euf_Checker.Name_BBExtract. +Register Euf_Checker.Name_BBZextend as SMTCoq.Trace.Euf_Checker.Name_BBZextend. +Register Euf_Checker.Name_BBSextend as SMTCoq.Trace.Euf_Checker.Name_BBSextend. +Register Euf_Checker.Name_BBShl as SMTCoq.Trace.Euf_Checker.Name_BBShl. +Register Euf_Checker.Name_BBShr as SMTCoq.Trace.Euf_Checker.Name_BBShr. +Register Euf_Checker.Name_RowEq as SMTCoq.Trace.Euf_Checker.Name_RowEq. +Register Euf_Checker.Name_RowNeq as SMTCoq.Trace.Euf_Checker.Name_RowNeq. +Register Euf_Checker.Name_Ext as SMTCoq.Trace.Euf_Checker.Name_Ext. +Register Euf_Checker.Name_Hole as SMTCoq.Trace.Euf_Checker.Name_Hole. +Register Euf_Checker.step as SMTCoq.Trace.Euf_Checker.step. +Register Euf_Checker.Res as SMTCoq.Trace.Euf_Checker.Res. +Register Euf_Checker.Weaken as SMTCoq.Trace.Euf_Checker.Weaken. +Register Euf_Checker.ImmFlatten as SMTCoq.Trace.Euf_Checker.ImmFlatten. +Register Euf_Checker.CTrue as SMTCoq.Trace.Euf_Checker.CTrue. +Register Euf_Checker.CFalse as SMTCoq.Trace.Euf_Checker.CFalse. +Register Euf_Checker.BuildDef as SMTCoq.Trace.Euf_Checker.BuildDef. +Register Euf_Checker.BuildDef2 as SMTCoq.Trace.Euf_Checker.BuildDef2. +Register Euf_Checker.BuildProj as SMTCoq.Trace.Euf_Checker.BuildProj. +Register Euf_Checker.ImmBuildProj as SMTCoq.Trace.Euf_Checker.ImmBuildProj. +Register Euf_Checker.ImmBuildDef as SMTCoq.Trace.Euf_Checker.ImmBuildDef. +Register Euf_Checker.ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.ImmBuildDef2. +Register Euf_Checker.EqTr as SMTCoq.Trace.Euf_Checker.EqTr. +Register Euf_Checker.EqCgr as SMTCoq.Trace.Euf_Checker.EqCgr. +Register Euf_Checker.EqCgrP as SMTCoq.Trace.Euf_Checker.EqCgrP. +Register Euf_Checker.LiaMicromega as SMTCoq.Trace.Euf_Checker.LiaMicromega. +Register Euf_Checker.LiaDiseq as SMTCoq.Trace.Euf_Checker.LiaDiseq. +Register Euf_Checker.SplArith as SMTCoq.Trace.Euf_Checker.SplArith. +Register Euf_Checker.SplDistinctElim as SMTCoq.Trace.Euf_Checker.SplDistinctElim. +Register Euf_Checker.BBVar as SMTCoq.Trace.Euf_Checker.BBVar. +Register Euf_Checker.BBConst as SMTCoq.Trace.Euf_Checker.BBConst. +Register Euf_Checker.BBOp as SMTCoq.Trace.Euf_Checker.BBOp. +Register Euf_Checker.BBNot as SMTCoq.Trace.Euf_Checker.BBNot. +Register Euf_Checker.BBEq as SMTCoq.Trace.Euf_Checker.BBEq. +Register Euf_Checker.BBDiseq as SMTCoq.Trace.Euf_Checker.BBDiseq. +Register Euf_Checker.BBNeg as SMTCoq.Trace.Euf_Checker.BBNeg. +Register Euf_Checker.BBAdd as SMTCoq.Trace.Euf_Checker.BBAdd. +Register Euf_Checker.BBMul as SMTCoq.Trace.Euf_Checker.BBMul. +Register Euf_Checker.BBUlt as SMTCoq.Trace.Euf_Checker.BBUlt. +Register Euf_Checker.BBSlt as SMTCoq.Trace.Euf_Checker.BBSlt. +Register Euf_Checker.BBConcat as SMTCoq.Trace.Euf_Checker.BBConcat. +Register Euf_Checker.BBExtract as SMTCoq.Trace.Euf_Checker.BBExtract. +Register Euf_Checker.BBZextend as SMTCoq.Trace.Euf_Checker.BBZextend. +Register Euf_Checker.BBSextend as SMTCoq.Trace.Euf_Checker.BBSextend. +Register Euf_Checker.BBShl as SMTCoq.Trace.Euf_Checker.BBShl. +Register Euf_Checker.BBShr as SMTCoq.Trace.Euf_Checker.BBShr. +Register Euf_Checker.RowEq as SMTCoq.Trace.Euf_Checker.RowEq. +Register Euf_Checker.RowNeq as SMTCoq.Trace.Euf_Checker.RowNeq. +Register Euf_Checker.Ext as SMTCoq.Trace.Euf_Checker.Ext. +Register Euf_Checker.Hole as SMTCoq.Trace.Euf_Checker.Hole. +Register Euf_Checker.ForallInst as SMTCoq.Trace.Euf_Checker.ForallInst. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) |