5 files changed, 11 insertions, 11 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 2eb2c3812..c2035586f 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -164,7 +164,7 @@ and ct_COMMAND =
   | CT_resume of ct_ID_OPT
   | CT_save of ct_THM_OPT * ct_ID_OPT
   | CT_scomments of ct_SCOMMENT_CONTENT_LIST
-  | CT_search of ct_ID * ct_IN_OR_OUT_MODULES
+  | CT_search of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_about of ct_ID_OR_STRING_NE_LIST * ct_IN_OR_OUT_MODULES
   | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 51dce4f76..79fa912a6 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -565,14 +565,14 @@ let pcoq_search s l =
       raw_search_about (filter_by_module_from_list l) add_search
 	(List.map (on_snd interp_search_about_item) sl)
   | SearchPattern c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
   | SearchRewrite c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       raw_search_rewrite (filter_by_module_from_list l) add_search pat;
-  | SearchHead locqid ->
-      filtered_search
-	(filter_by_module_from_list l) add_search (Nametab.global locqid)
+  | SearchHead c ->
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+      raw_search_by_head (filter_by_module_from_list l) add_search pat;
   end;
   search_output_results()
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index d6ef1ea3b..5180bdad2 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib =
   let _, l =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
-  VernacInductive (mib.mind_finite, l)
+  VernacInductive (mib.mind_finite, false, l)
   :: (implicit_args_to_ast_list sp mipv);;
 
 let constr_to_ast v = 
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 946090099..b9daf6357 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -530,7 +530,7 @@ and fCOMMAND = function
    fSCOMMENT_CONTENT_LIST x1 ++
    fNODE "scomments" 1
 | CT_search(x1, x2) ->
-   fID x1 ++
+   fFORMULA x1 ++
    fIN_OR_OUT_MODULES x2 ++
    fNODE "search" 2
 | CT_search_about(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ee48ee53b..6b65fbcc5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1950,8 +1950,8 @@ let rec xlate_vernac =
       (match s with
 	| SearchPattern c ->
 	    CT_search_pattern(xlate_formula c, translated_restriction)
-	| SearchHead id ->
-	    CT_search(loc_qualid_to_ct_ID id, translated_restriction)
+	| SearchHead c ->
+	    CT_search(xlate_formula c, translated_restriction)
 	| SearchRewrite c ->
 	    CT_search_rewrite(xlate_formula c, translated_restriction)
 	| SearchAbout (a::l) ->
@@ -1984,7 +1984,7 @@ let rec xlate_vernac =
 (*         xlate_ident s, xlate_binder_list binders,  *)
 (* 	xlate_formula (Option.get c1), record_constructor, *)
 (*          build_record_field_list field_list) *)
-   | VernacInductive (isind, lmi) ->
+   | VernacInductive (isind, _, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
       let strip_mutind = function
           (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->