diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-18 18:01:20 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-18 18:01:20 +0100 |
| commit | bfce2747a747f48465fe32c3d29304ca6e774f25 (patch) | |
| tree | 6baf459718c380e90b76b5938e625ca0272a58e4 /src/trace/smtCommands.ml | |
| parent | 23539f231727113d53e4fdeae531d048b21730ae (diff) | |
| download | smtcoq-bfce2747a747f48465fe32c3d29304ca6e774f25.tar.gz smtcoq-bfce2747a747f48465fe32c3d29304ca6e774f25.zip | |
Light port to Coq 8.5 under progress
Diffstat (limited to 'src/trace/smtCommands.ml')
| -rw-r--r-- | src/trace/smtCommands.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 1941065..52450d1 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -177,8 +177,8 @@ let build_body rt ro ra rf l b (max_id, confl) = Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], mklApp cchecker_b_correct [|vti;vtfunc;vtatom; vtform; l; b; vc; vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|]))))) @@ -209,8 +209,8 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], mklApp cchecker_eq_correct [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc; vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|]))))) |