diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 18:30:16 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 18:30:16 +0100 |
commit | 78167cc85a2f580691ef08ce8ccd3391158167d3 (patch) | |
tree | 824c19dbde77ca00b7e345daa77921484feaf519 /src/trace | |
parent | 7072c4591668d2c21211a744d3719f6b42d1e7b9 (diff) | |
download | smtcoq-78167cc85a2f580691ef08ce8ccd3391158167d3.tar.gz smtcoq-78167cc85a2f580691ef08ce8ccd3391158167d3.zip |
Identify ML functions that are implemented differently in native-coq and in standard coq
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/coqTerms.ml | 2 | ||||
-rw-r--r-- | src/trace/smtMisc.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 8046a47..d71ba45 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -170,7 +170,7 @@ let make_certif_ops modules = gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim") -(** Usefull construction *) +(** Useful construction *) let ceq_refl_true = lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|]) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 849c0d7..893a9be 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -35,11 +35,11 @@ let mklApp f args = Term.mkApp (Lazy.force f, args) let coqtype = lazy Term.mkSet let declare_new_type t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Pp.dummy_loc,t); + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Structures.dummy_loc,t); Term.mkVar t let declare_new_variable v constr_t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Pp.dummy_loc,v); + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Structures.dummy_loc,v); Term.mkVar v let mkName s = |