diff options
| author | Pierre-Marie Pédrot | 2019-12-08 12:45:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-10 10:53:53 +0100 |
| commit | 504b1b71ed56431c978b9bbf46c4d67f155fddf2 (patch) | |
| tree | 1f09da98c5110a2f2506c0cee4e6cc6ab4ea0c6a /vernac | |
| parent | 0ad6e13fc3065c6ff1eefa87c8a709fdf5602b0a (diff) | |
Simplify internal flags in scheme declarations.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 310ea62a1d..f954915cf8 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = end (* used in the bool -> leb side *) -let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let open EConstr in let avoid = Array.of_list aavoid in let do_arg sigma hd v offset = @@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") then Tacticals.New.tclTHEN - (do_replace_bl mode bl_scheme_key ind + (do_replace_bl bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) |