From a5bd782f300c3767936fc3f45df6a09cda185370 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 26 Apr 2016 23:07:38 +0200 Subject: Both native-coq and Coq 8.5 are fully supported --- src/verit/veritSyntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/verit/veritSyntax.ml') diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index 3ff11e9..33c059d 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -136,7 +136,7 @@ let mkCongrPred p = Other (EqCgrP (p_p,c,cert)) else failwith "VeritSyntax.mkCongrPred: unmatching predicates" | _ -> failwith "VeritSyntax.mkCongrPred : not pred app") - |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premice in congruence") + |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence") |[] -> failwith "VeritSyntax.mkCongrPred: no conclusion in congruence" |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence" -- cgit