diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-04 16:55:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-04 16:55:56 +0200 |
| commit | c112063ba5f562d511ed0cbd754a41539fc48fe1 (patch) | |
| tree | 1f7e244b3d3b0963d07463604d77bdf35001e67c /plugins/ltac | |
| parent | b824d8ad00001f6c41d0fc8bbf528dccb937c887 (diff) | |
| parent | ea10a2da9ac11ea57e9eb80d0d6baf9321886da4 (diff) | |
Merge branch 'trunk' into pr379
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 6 |
4 files changed, 7 insertions, 5 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index aab568746..fd33a779d 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 diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index d286a5870..3e6e2db60 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 diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb..c50100bf5 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 10fec2032..7a20838a2 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -78,17 +78,17 @@ val is_applied_rewrite_relation : env -> evar_map -> rel_context -> 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 |