diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
commit | ff9b5494cb1943339543eeac41683a8ec2dda437 (patch) | |
tree | 21af4c0fff64fbd03c6c2006da1e305e849ebbff /src/Trace.v | |
parent | 5311b1fa064949089b8d17e34eb31a62426f71fd (diff) | |
download | smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.tar.gz smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.zip |
More on the support for standard Coq (not working yet)
Diffstat (limited to 'src/Trace.v')
-rw-r--r-- | src/Trace.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Trace.v b/src/Trace.v index d369958..7930a83 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -51,7 +51,7 @@ Section trace. Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool := let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in is_false (S.get s' confl). - Register _checker_ as PrimInline. + (* Register _checker_ as PrimInline. *) (* For debugging *) (* |