diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:36:55 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:36:55 +0200 |
| commit | 6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6 (patch) | |
| tree | 8de224f14b73cd34bd81ce18f251ba0cdfe0bb64 /src/trace/smtCommands.ml | |
| parent | 87ec8048b9da841af7b124b6dc91c9a8550b7585 (diff) | |
| download | smtcoq-6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6.tar.gz smtcoq-6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6.zip | |
Compatibility with native-coq
Diffstat (limited to 'src/trace/smtCommands.ml')
| -rw-r--r-- | src/trace/smtCommands.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 943e634..53ea75c 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -134,7 +134,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) = (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in let ce = Structures.mkConst theorem_proof in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in - () + () (* Given an SMT-LIB2 file and a certif, call the checker *) @@ -219,8 +219,8 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = let get_arguments concl = let f, args = Term.decompose_app concl in match args with - | [ty;a;b] when (Constr.equal f (Lazy.force ceq)) && (Constr.equal ty (Lazy.force cbool)) -> a, b - | [a] when (Constr.equal f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Verit.tactic: can only deal with equality over bool") @@ -239,9 +239,9 @@ let tactic call_solver rt ro ra rf gl = let env = Environ.push_rel_context forall_let env in let a, b = get_arguments concl in let body = - if ((Constr.equal b (Lazy.force ctrue)) || (Constr.equal b (Lazy.force cfalse))) then + if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in - let l' = if (Constr.equal b (Lazy.force ctrue)) then Form.neg l else l in + let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let max_id_confl = make_proof call_solver rt ro rf l' in build_body rt ro ra rf (Form.to_coq l) b max_id_confl else |