diff options
| author | Maxime Dénès | 2017-04-03 15:21:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-03 15:22:40 +0200 |
| commit | 9da03d38249a2716e7ede5d20948759e6d975138 (patch) | |
| tree | d6666937b32e3b65e71caaf4511f164e7818ef04 /plugins/ltac | |
| parent | 3fe764dd8d6578adddb01b02bafc7f31d9cb776c (diff) | |
| parent | eec5145a5c6575d04b5ab442597fb52913daed29 (diff) | |
Merge PR#417: No cast surgery in let in
Diffstat (limited to 'plugins/ltac')
| -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 |
3 files changed, 5 insertions, 5 deletions
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 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 |