Cleanup

5 files changed, 3 insertions, 49 deletions

diff --git a/README-JFLA19.md b/README-JFLA19.md
deleted file mode 100644
index 40ac5b5..0000000
--- a/README-JFLA19.md
+++ /dev/null
@@ -1,40 +0,0 @@
-# README for the submission to the [JFLA conference 2019](https://dpt-info.u-strasbg.fr/~magaud/JFLA2019)
-
-This README is related to the submission of an article to the [JFLA conference 2019](https://dpt-info.u-strasbg.fr/~magaud/JFLA2019). It is intentionaly written in French.
-
-
-## Installation
-
-Il faut utiliser l'installation à partir des sources décrite dans [ce fichier](https://github.com/smtcoq/smtcoq/blob/master/INSTALL.md).
-
-Une nouvelle release, ainsi que la mise à jour du paquet opam, sont prévues courant novembre.
-
-
-## Utilisation
-
-Le fichier [examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v) donne un aperçu des possibilités offertes par SMTCoq. La fin du fichier présente des exemples sur les éléments présentés dans la soumission.
-
-
-## Description des éléments présentés dans la soumission
-### Ajout de lemmes quantifiés
-
-La fin du fichier [examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v) (lignes 154 à fin) présente différentes utilisations décrites en introduction et dans la section 3.5.
-
-Côté Coq:
-
-- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/Trace.v](https://github.com/smtcoq/smtcoq/blob/master/src/Trace.v). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 344. Sa propriété de correction est prouvée dans le fichier [src/spl/Assumptions.v](https://github.com/smtcoq/smtcoq/blob/master/src/spl/Assumptions.v).
-
-- Le cas d'application à la tactique `verit` (§ 3.4.3) est définie dans le fichier [src/SMTCoq.v](https://github.com/smtcoq/smtcoq/blob/master/src/SMTCoq.v), avec la définition de la tactique `vauto` permettant la preuve automatique des instanciations.
-
-Côté OCaml:
-
-- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/trace/smtCertif.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtCertif.ml). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 113. Son traitement est donné dans le fichier [src/trace/smtTrace.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtTrace.ml), ligne 423.
-
-- Le préprocesseur pour la règle forall_inst de veriT (§ 3.4.2 et 3.4.3) est défini dans le fichier [src/verit/veritSyntax.ml](https://github.com/smtcoq/smtcoq/blob/master/src/verit/veritSyntax.ml), lignes 213 et suivantes.
-
-
-### Traductions entre représentations des données
-
-Le fichier [examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v) (lignes 71 à 150) présente différentes utilisations décrites dans la section 4.
-
-L'implantation de ces tactiques est donnée par le fichier documenté [src/Conversion_tactics.v](https://github.com/smtcoq/smtcoq/blob/master/src/Conversion_tactics.v).
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