From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 plugins/ltac/g_rewrite.ml4 | 2 +-
 plugins/ltac/rewrite.mli   | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb8..c50100bf55 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
       [ declare_relation a aeq n None None (Some lemma3) ]
 END
 
-type binders_argtype = local_binder list
+type binders_argtype = local_binder_expr list
 
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35c4483513..4fdce0c84f 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -77,17 +77,17 @@ val is_applied_rewrite_relation :
   env -> evar_map -> Context.Rel.t -> constr -> types option
 
 val declare_relation :
-  ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
+  ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
   constr_expr option -> constr_expr option -> constr_expr option -> unit
 
 val add_setoid :
-  bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr ->
+  bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> unit
 
 val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
 
 val add_morphism :
-  bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit
+  bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
-- 
cgit v1.2.3


From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:24:58 +0100
Subject: Unifying standard "constr_level" names for constructors of
 local_binder_expr.

RawLocal -> CLocal
---
 plugins/ltac/g_obligations.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a58708..3e6e2db605 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -70,7 +70,7 @@ GEXTEND Gram
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
+          [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
   END
-- 
cgit v1.2.3


From 05421cef04206a18cb30f6d115d27e7cb25ba0bf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 30 Mar 2017 10:09:01 +0200
Subject: Declaring ltac plugin, so that static linking works.

---
 plugins/ltac/g_ltac.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index aab5687465..fd33a779dc 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "ltac_plugin"
+
 open Util
 open Pp
 open Compat
-- 
cgit v1.2.3