aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtMisc.ml
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-04-21 10:00:58 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2021-04-21 10:00:58 +0200
commit13d2c8be2ffb84bc8d40064b223562832e5a5a7e (patch)
tree8e9b4c8b8c31ee95bcd7eeffaacf72b40215adb3 /src/trace/smtMisc.ml
parent0955c9b404b2bebbe76a15daaad09c03670e849e (diff)
parent4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (diff)
downloadsmtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.tar.gz
smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.zip
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/trace/smtMisc.ml')
-rw-r--r--src/trace/smtMisc.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 607ebe7..d33a0ec 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -23,8 +23,8 @@ let mkInt i =
(** Generic representation of shared object *)
type 'a gen_hashed = { index : int; hval : 'a }
-(** Functions over constr *)
+(** Functions over constr *)
let mklApp f args = Structures.mkApp (Lazy.force f, args)
let string_of_name_def d n = try Structures.string_of_name n with | _ -> d