diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-03-31 20:25:05 +0200 |
| commit | 20831b39a73ebd38336f19ad4ddb4d6b1078d60d (patch) | |
| tree | 9e4ec27753feff8f7e95274f99eaa977b546c030 /src/trace/smtCommands.ml | |
| parent | 4c8654c57666e27637ba2f60ee5c6455176c7a1d (diff) | |
| download | smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.tar.gz smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.zip | |
Compiles with Coq-8.10
Diffstat (limited to 'src/trace/smtCommands.ml')
| -rw-r--r-- | src/trace/smtCommands.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index e64a131..b1f2666 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) = let tf = Hashtbl.create 17 in let rec interp = function | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|] - | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in + | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in interp prem |