diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2019-01-29 14:51:31 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2019-01-29 14:51:31 +0100 |
| commit | 3165bb9c1853cd2e471e28c52418dee865d181c3 (patch) | |
| tree | 35bd4edf8afe2b1d6773e435b07b887ca509338c /src | |
| parent | 7021c53d4ecf97c82ccebb6bb45f5305d8b482ea (diff) | |
| download | smtcoq-3165bb9c1853cd2e471e28c52418dee865d181c3.tar.gz smtcoq-3165bb9c1853cd2e471e28c52418dee865d181c3.zip | |
Cleanup
Diffstat (limited to 'src')
| -rw-r--r-- | src/trace/smtBtype.ml | 2 | ||||
| -rw-r--r-- | src/trace/smtBtype.mli | 2 | ||||
| -rw-r--r-- | src/versions/standard/structures.ml | 4 | ||||
| -rw-r--r-- | src/versions/standard/structures.mli | 4 |
4 files changed, 3 insertions, 9 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 8580ed0..0ebb893 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -77,7 +77,7 @@ let rec logic = function type reify_tbl = { mutable count : int; tbl : (Term.constr, btype) Hashtbl.t; - mutable cuts : (Structures.names_id_t * Term.types) list; + mutable cuts : (Structures.names_id * Term.types) list; unsup_tbl : (btype, btype) Hashtbl.t; } diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 559e809..4f8d4ad 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -59,6 +59,6 @@ val interp : Term.constr -> btype -> Term.constr val interp_to_coq : reify_tbl -> btype -> Term.constr -val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list +val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list val logic : btype -> logic diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 3dbcad2..cf5a272 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -75,8 +75,6 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Differences between the two versions of Coq *) -type names_id_t = Names.Id.t - let dummy_loc = Loc.ghost let mkUConst c = @@ -131,8 +129,6 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty let lift = Vars.lift -type rel_decl = Context.Rel.Declaration.t - let destruct_rel_decl r = Context.Rel.Declaration.get_name r, Context.Rel.Declaration.get_type r diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index f7c4f91..b17aa3c 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -33,7 +33,6 @@ val mkTrace : Term.constr Lazy.t -> Term.constr Lazy.t -> int -> Term.constr -> Term.constr -> 'a ref -> Term.constr -type names_id_t = Names.Id.t val dummy_loc : Loc.t val mkUConst : Term.constr -> Safe_typing.private_constants Entries.definition_entry @@ -49,8 +48,7 @@ val extern_constr : Term.constr -> Constrexpr.constr_expr val vernacentries_interp : Constrexpr.constr_expr -> unit val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds val lift : int -> Constr.constr -> Constr.constr -type rel_decl = Context.Rel.Declaration.t -val destruct_rel_decl : rel_decl -> Names.Name.t * Constr.t +val destruct_rel_decl : Context.Rel.Declaration.t -> Names.Name.t * Constr.t val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr val tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic |