- Relâchement de la contrainte de bonne longueur des intropatterns

  lorsqu'en position terminale (en fait, l'idéal serait de pouvoir
  mettre des tactiques dans les branches, style "intros [H ; tac | ]")
  (cf un exemple QvMake.v)
- Pas de delta du tout quand on fait de la recherche de sous-terme
  (même lorsqu'on vient de apply avec une conclusion ?P t) (cf un
  exemple dans Rocq/DEMOS/Sorting.v)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7

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)