diff options
| -rw-r--r-- | parsing/q_coqast.ml4 | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 13 |
3 files changed, 11 insertions, 7 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 55b5315851..d961dc2f2e 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -67,12 +67,13 @@ let mlexpr_of_by_notation f = function | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> let mlexpr_of_intro_pattern = function - | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> | Genarg.IntroIdentifier id -> <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ -> + failwith "mlexpr_of_intro_pattern: TODO" let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3ef17778a9..b1a4c3b8c7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -633,6 +633,8 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd = (evd,[]) let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = + (* Remove delta when looking for a subterm *) + let flags = { flags with modulo_delta = Cpred.empty } in let (evd',cllist) = w_unify_to_subterm_list env flags allow_K oplist typ evd in let typp = Typing.meta_type evd' p in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a2ec3705e..ac72c4479d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -984,17 +984,18 @@ let intro_or_and_pattern ll l' tac = tclLAST_HYP (fun c gl -> let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let nv = mis_constr_nargs ind in - let rec adjust_names_length force n = function - | [] when n = 0 or not force -> [] - | [] -> IntroAnonymous :: adjust_names_length force (n-1) [] - | _ :: _ when n = 0 -> error "Too many names in some branch" - | ip :: l -> ip :: adjust_names_length force (n-1) l in + let rec adjust_names_length tail n = function + | [] when n = 0 or tail -> [] + | [] -> IntroAnonymous :: adjust_names_length tail (n-1) [] + | _ :: _ as l when n = 0 -> + if tail then l else error "Too many names in some branch" + | ip :: l -> ip :: adjust_names_length tail (n-1) l in let ll = fix_empty_case nv ll in if List.length ll <> Array.length nv then error "Not the right number of patterns"; tclTHENLASTn (tclTHEN case_last clear_last) - (array_map2 (fun n l -> tac ((adjust_names_length (l'<>[]) n l)@l')) + (array_map2 (fun n l -> tac ((adjust_names_length (l'=[]) n l)@l')) nv (Array.of_list ll)) gl) |