Laxer dependencies between file and link reordering.

5 files changed, 9 insertions, 20 deletions

diff --git a/_CoqProject b/_CoqProject
index f202e1aed2..4116d17554 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,11 +15,11 @@ src/tac2entries.ml
 src/tac2entries.mli
 src/tac2ffi.ml
 src/tac2ffi.mli
-src/tac2core.ml
-src/tac2core.mli
 src/tac2qexpr.mli
 src/tac2quote.ml
 src/tac2quote.mli
+src/tac2core.ml
+src/tac2core.mli
 src/tac2tactics.ml
 src/tac2tactics.mli
 src/tac2stdlib.ml
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 4c4082ad65..f9fa2fafd8 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -4,8 +4,8 @@ Tac2intern
 Tac2interp
 Tac2entries
 Tac2ffi
-Tac2core
 Tac2quote
+Tac2core
 Tac2tactics
 Tac2stdlib
 G_ltac2
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 3ce2ed53a8..bf41713215 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -45,10 +45,6 @@ let c_some = coq_core "Some"
 let c_true = coq_core "true"
 let c_false = coq_core "false"
 
-let t_qhyp = std_core "hypothesis"
-let c_named_hyp = std_core "NamedHyp"
-let c_anon_hyp = std_core "AnonHyp"
-
 end
 
 open Core
diff --git a/src/tac2core.mli b/src/tac2core.mli
index 6fd48e85f7..d9ed8ea2e5 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -27,8 +27,4 @@ val t_array : type_constant
 val c_true : ltac_constructor
 val c_false : ltac_constructor
 
-val t_qhyp : type_constant
-val c_anon_hyp : ltac_constructor
-val c_named_hyp : ltac_constructor
-
 end
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index b3d174dc2d..8adeb15d20 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -9,18 +9,15 @@
 open Pp
 open Names
 open Util
-open Misctypes
-open Tac2intern
 open Tac2expr
 open Tac2qexpr
-open Tac2core
 
 (** Syntactic quoting of expressions. *)
 
 let control_prefix =
   MPfile (DirPath.make (List.map Id.of_string ["Control"; "Ltac2"]))
 
-let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string n))
+let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string_soft n))
 let std_core n = kername Tac2env.std_prefix n
 let coq_core n = kername Tac2env.coq_prefix n
 let control_core n = kername control_prefix n
@@ -86,17 +83,17 @@ let of_open_constr c =
   inj_wit ?loc Stdarg.wit_open_constr c
 
 let of_bool ?loc b =
-  let c = if b then Core.c_true else Core.c_false in
+  let c = if b then coq_core "true" else coq_core "false" in
   constructor ?loc c []
 
 let rec of_list ?loc f = function
-| [] -> constructor Core.c_nil []
+| [] -> constructor (coq_core "[]") []
 | e :: l ->
-  constructor ?loc Core.c_cons [f e; of_list ?loc f l]
+  constructor ?loc (coq_core "::") [f e; of_list ?loc f l]
 
 let of_qhyp (loc, h) = match h with
-| QAnonHyp n -> constructor ?loc Core.c_anon_hyp [of_int n]
-| QNamedHyp id -> constructor ?loc Core.c_named_hyp [of_ident id]
+| QAnonHyp n -> std_constructor ?loc "AnonHyp" [of_int n]
+| QNamedHyp id -> std_constructor ?loc "NamedHyp" [of_ident id]
 
 let of_bindings (loc, b) = match b with
 | QNoBindings ->