Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

16 files changed, 181 insertions, 133 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1212656b..36136a6c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: auto.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -150,10 +150,13 @@ module Hint_db = struct
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
       
+  let map_none db = 
+    Sort.merge pri_order db.hintdb_nopat []
+      
   let map_all k db =
     let (l,l',_) = find k db in
       Sort.merge pri_order (db.hintdb_nopat @ l) l'
-   
+
   let map_auto (k,c) db =
     let st = if db.use_dn then Some db.hintdb_state else None in
     let l' = lookup_tacs (k,c) st (find k db) in
@@ -637,26 +640,24 @@ let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
 let pr_hint_term cl = 
   try 
-    let (hdc,args) = head_constr_bound cl in
-    let hd = head_of_constr_reference hdc in
     let dbs = Hintdbmap.to_list !searchtable in
     let valid_dbs = 
-      if occur_existential cl then 
-	map_succeed 
-	  (fun (name, db) -> (name, db, Hint_db.map_all hd db)) 
-	  dbs
-      else 
-	map_succeed 
-	  (fun (name, db) -> 
-	     (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) 
-	  dbs
-    in 
-    if valid_dbs = [] then 
-      (str "No hint applicable for current goal")
-    else
-      (str "Applicable Hints :" ++ fnl () ++
-	 hov 0 (prlist pr_hints_db valid_dbs))
-  with Bound | Match_failure _ | Failure _ -> 
+      let fn = try 
+	  let (hdc,args) = head_constr_bound cl in
+	  let hd = head_of_constr_reference hdc in
+	    if occur_existential cl then
+	      Hint_db.map_all hd
+	    else Hint_db.map_auto (hd, applist (hdc,args))
+	with Bound -> Hint_db.map_none
+      in
+	map_succeed (fun (name, db) -> (name, db, fn db)) dbs
+    in
+      if valid_dbs = [] then 
+	(str "No hint applicable for current goal")
+      else
+	(str "Applicable Hints :" ++ fnl () ++
+	    hov 0 (prlist pr_hints_db valid_dbs))
+  with Match_failure _ | Failure _ -> 
     (str "No hint applicable for current goal")
 
 let error_no_such_hint_database x =
@@ -795,6 +796,13 @@ let flags_of_state st =
   {auto_unif_flags with 
     modulo_conv_on_closed_terms = Some st; modulo_delta = st}
 
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> Hint_db.map_none
+  | Some hdc ->
+      if occur_existential concl then Hint_db.map_all hdc
+      else Hint_db.map_auto (hdc,concl)
+	
 let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
@@ -808,12 +816,8 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
        (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
 and my_find_search_nodelta db_list local_db hdc concl =
-  if occur_existential concl then
-    List.map (fun hint -> (None,hint))
-      (list_map_append (Hint_db.map_all hdc) (local_db::db_list))
-  else
-    List.map (fun hint -> (None,hint))
-      (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list))
+  List.map (fun hint -> (None,hint)) 
+    (list_map_append (hintmap_of hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
@@ -821,28 +825,31 @@ and my_find_search mod_delta =
     
 and my_find_search_delta db_list local_db hdc concl =
   let flags = {auto_unif_flags with use_metas_eagerly = true} in
+  let f = hintmap_of hdc concl in
     if occur_existential concl then 
       list_map_append
 	(fun db -> 
 	  if Hint_db.use_dn db then 
 	    let flags = flags_of_state (Hint_db.transparent_state db) in
-	      List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	      List.map (fun x -> (Some flags,x)) (f db)
 	  else
 	    let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
-	      List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db))
+	      List.map (fun x -> (Some flags,x)) (f db))
 	(local_db::db_list)
     else
       list_map_append (fun db -> 
 	if Hint_db.use_dn db then 
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
-	    List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	    List.map (fun x -> (Some flags, x)) (f db)
 	else
 	  let (ids, csts as st) = Hint_db.transparent_state db in
 	  let flags, l =
 	    let l =
-	      if (Idpred.is_empty ids && Cpred.is_empty csts)
-	      then Hint_db.map_auto (hdc,concl) db
-	      else Hint_db.map_all hdc db
+	      match hdc with None -> Hint_db.map_none db
+	      | Some hdc ->
+		  if (Idpred.is_empty ids && Cpred.is_empty csts)
+		  then Hint_db.map_auto (hdc,concl) db
+		  else Hint_db.map_all hdc db
 	    in {flags with modulo_delta = st}, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
@@ -861,13 +868,15 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       
 and trivial_resolve mod_delta db_list local_db cl = 
   try 
-    let hdconstr,_ = head_constr_bound cl in
-    List.map (tac_of_hint db_list local_db cl)
-      (priority 
-	(my_find_search mod_delta db_list local_db
-	  (head_of_constr_reference hdconstr) cl))
-  with Bound | Not_found -> 
-    []
+    let head = 
+      try let hdconstr,_ = head_constr_bound cl in
+	    Some (head_of_constr_reference hdconstr)
+      with Bound -> None
+    in
+      List.map (tac_of_hint db_list local_db cl)
+	(priority 
+	    (my_find_search mod_delta db_list local_db head cl))
+  with Not_found -> []
 
 let trivial lems dbnames gl =
   let db_list = 
@@ -903,12 +912,14 @@ let h_trivial lems l =
 
 let possible_resolve mod_delta db_list local_db cl =
   try 
-    let hdconstr,_ = head_constr_bound cl in
-    List.map (tac_of_hint db_list local_db cl)
-      (my_find_search mod_delta db_list local_db
-        (head_of_constr_reference hdconstr) cl)
-  with Bound | Not_found -> 
-    []
+    let head = 
+      try let hdconstr,_ = head_constr_bound cl in
+	    Some (head_of_constr_reference hdconstr)
+      with Bound -> None
+    in
+      List.map (tac_of_hint db_list local_db cl)
+	(my_find_search mod_delta db_list local_db head cl)
+  with Not_found -> []
 
 let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c9065ef3..132b9063 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: auto.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id: auto.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -53,6 +53,7 @@ module Hint_db :
     type t
     val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
+    val map_none : t -> pri_auto_tactic list
     val map_all : global_reference -> t -> pri_auto_tactic list
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
     val add_one : hint_entry -> t -> t
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6a425984..b7eb3620 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: class_tactics.ml4 12189 2009-06-15 05:08:44Z msozeau $ *)
 
 open Pp
 open Util
@@ -46,18 +46,18 @@ let typeclasses_db = "typeclass_instances"
 let _ = Auto.auto_init := (fun () -> 
   Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
-let check_imported_library d =
+let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
   if not (Library.library_is_loaded dir) then
-    error ("Library "^(list_last d)^" has to be imported first.")
+    error ("Library "^(list_last d)^" has to be required first.")
       
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
   
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
-  else check_imported_library ["Coq";"Setoids";"Setoid"]
+  else check_required_library ["Coq";"Setoids";"Setoid"]
 
 (** Typeclasses instance search tactic / eauto *)
 
@@ -245,7 +245,6 @@ module SearchProblem = struct
 	    Option.iter (fun r ->
 (*  	      msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
 	      r := true) do_cut;
-	  let sigma = Evarutil.nf_evars sigma in
 	  let gl = List.map (Evarutil.nf_evar_info sigma) gl in
 	  let nbgl = List.length gl in
 (* 	  let gl' = { it = gl ; sigma = sigma } in *)
@@ -338,6 +337,7 @@ let is_transparent_gr (ids, csts) = function
   | IndRef _ | ConstructRef _ -> false
 
 let make_resolve_hyp env sigma st flags pri (id, _, cty) =
+  let cty = Evarutil.nf_evar sigma cty in
   let ctx, ar = decompose_prod cty in
   let keep = 
     match kind_of_term (fst (decompose_app ar)) with
@@ -625,9 +625,6 @@ let is_applied_setoid_relation t =
 let _ = 
   Equality.register_is_applied_setoid_relation is_applied_setoid_relation
 
-exception Found of (constr * constr * (types * types) list * constr * constr array *
-		       (constr * (constr * constr * constr * constr)) option array)
-
 let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
@@ -1675,7 +1672,7 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl =
   let bindings = Tacinterp.interp_bindings my_ist gl bl in
     typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type
 
-let typeclass_app_raw t gl =
+let typeclass_app_raw (_,t) gl =
   let env = pf_env gl in
   let evars = ref (create_evar_defs (project gl)) in
   let j = Pretyping.Default.understand_judgment_tcc evars env t in
@@ -1715,7 +1712,7 @@ END
 
 let not_declared env ty rel =
   tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ 
-		str ty ++ str" relation. Maybe you need to import the Setoid library")
+		str ty ++ str" relation. Maybe you need to require the Setoid library")
 
 let relation_of_constr env c = 
   match kind_of_term c with
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 2d0395a3..62a8ddfc 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
 
 open Util
 open Pp
@@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt =
 let mark_as_done pts = 
   map_pftreestate 
     (fun _ -> mark_proof_tree_as_done) 
-    (traverse 0 pts) 
+    (up_to_matching_rule is_focussing_command pts) 
 
 (* post-instruction focus management *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index baebee07..58a00419 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
 
 open Pp
 open Util
@@ -1215,7 +1215,7 @@ let subst_one x gl =
        tclMAP introtac depdecls]) @
      [tclTRY (clear [x;hyp])]) gl
 
-let subst = tclMAP subst_one
+let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
 
 let subst_all gl =
   let test (_,c) =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 43c18a8b..67b89888 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_tactics.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: evar_tactics.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Term
 open Util
@@ -29,7 +29,7 @@ let evar_list evc c =
   in 
     evrec [] c
 
-let instantiate n rawc ido gl = 
+let instantiate n (ist,rawc) ido gl = 
   let sigma = gl.sigma in
   let evl = 
     match ido with
@@ -52,7 +52,9 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "Incorrect existential variable index.";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
+    let env = Evd.evar_env (Evd.find sigma ev) in
+    let ltac_vars = Tacinterp.extract_ltac_vars ist sigma env in
+    let evd' = w_refine ev (ltac_vars,rawc) (create_goal_evar_defs sigma) in
       tclTHEN
         (tclEVARS (evars_of evd'))
         tclNORMEVAR
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index cc06d2c6..f577b338 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_tactics.mli 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id: evar_tactics.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 open Tacmach
 open Names
 open Tacexpr
 open Termops
 
-val instantiate : int -> Rawterm.rawconstr -> 
+val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr -> 
   (identifier * hyp_location_flag, unit) location -> tactic
 
 (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 694c3495..5eb333a0 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extraargs.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: extraargs.ml4 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -100,9 +100,9 @@ END
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw
 
-let interp_raw _ _ (t,_) = t
+let interp_raw ist gl (t,_) = (ist,t)
 
 let glob_raw = Tacinterp.intern_constr
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index bccb150f..b64adf24 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraargs.mli 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: extraargs.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 open Tacexpr
 open Term
@@ -25,7 +25,7 @@ val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : rawconstr typed_abstract_argument_type
+val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type
 val raw : constr_expr Pcoq.Gram.Entry.e
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b270ba2d..8e517453 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Term
 open Proof_type
@@ -75,10 +75,6 @@ let h_generalize_dep c =
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
-let h_instantiate n c ido = 
-(Evar_tactics.instantiate n c ido)
-  (* abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 0ebb024a..9270411a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -62,8 +62,6 @@ val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_let_tac         : letin_flag -> name -> constr -> 
                         Tacticals.clause -> tactic
-val h_instantiate     : int -> Rawterm.rawconstr ->
-  (identifier * hyp_location_flag, unit) location -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index dff3b003..322d25e5 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -327,29 +327,31 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           gl
 
     (* fix => tactique Fix *)
-    | Fix ((ni,_),(fi,ai,_)) , _ ->
+    | Fix ((ni,j),(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
           | _ -> error "Recursive functions must have names."
 	in
 	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
+	let firsts,lasts = list_chop j (Array.to_list fixes) in
 	tclTHENS
-	  (mutual_fix (out_name fi.(0)) (succ ni.(0))
-	    (List.tl (Array.to_list fixes)))
+	  (mutual_fix_with_index 
+	    (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
     (* cofix => tactique CoFix *)
-    | CoFix (_,(fi,ai,_)) , _ ->
+    | CoFix (j,(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
           | _ -> error "Recursive functions must have names."
 	in
 	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
+	let firsts,lasts = list_chop j (Array.to_list cofixes) in
 	tclTHENS
-	  (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
+	  (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
@@ -366,10 +368,15 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
 (* Et finalement la tactique refine elle-même : *)
 
-let refine oc gl =
+let refine (evd,c) gl =
   let sigma = project gl in
-  let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+  let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
+			     ~onlyargs:true ~fail:false (pf_env gl) 
+			     (Evd.create_evar_defs evd)) 
+  in
+  let c = Evarutil.nf_evar evd c in
+  let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
   (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
      complicated to update meta types when passing through a binder *)
-  let th = compute_metamap (pf_env gl) sigma c in
-  tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
+  let th = compute_metamap (pf_env gl) evd c in
+  tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9026a6d..71b50b66 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Constrintern
 open Closure
@@ -539,7 +539,9 @@ let intern_induction_arg ist = function
   | ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
+	match intern_constr ist (CRef (Ident (dloc,id))) with
+	| RVar (loc,id),_ -> ElimOnIdent (loc,id)
+	| c -> ElimOnConstr (c,NoBindings)
       else
 	ElimOnIdent (loc,id)
 
@@ -1396,6 +1398,14 @@ let retype_list sigma env lst =
     try (x,Retyping.get_judgment_of env sigma csr)::a with
     | Anomaly _ -> a) lst []
 
+let extract_ltac_vars_data ist sigma env =
+  let (ltacvars,_ as vars) = constr_list ist env in
+  vars, retype_list sigma env ltacvars
+
+let extract_ltac_vars ist sigma env =
+  let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
+  typs,unbndltacvars
+
 let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1441,8 +1451,8 @@ let solve_remaining_evars env initial_sigma evd c =
   proc_rec (Evarutil.nf_isevar !evdref c)
 
 let interp_gen kind ist sigma env (c,ce) =
-  let (ltacvars,unbndltacvars as vars) = constr_list ist env in
-  let typs = retype_list sigma env ltacvars in
+  let (ltacvars,unbndltacvars as vars),typs =
+    extract_ltac_vars_data ist sigma env in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1717,10 +1727,20 @@ let interp_induction_arg ist gl = function
   | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
-      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
-      else ElimOnConstr
-	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
-	 NoBindings)
+      try
+	match List.assoc id ist.lfun with
+	| VInteger n -> ElimOnAnonHyp n
+	| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
+	| VConstr c -> ElimOnConstr (c,NoBindings)
+	| _ -> user_err_loc (loc,"",
+	      strbrk "Cannot coerce " ++ pr_id id ++
+	      strbrk " neither to a quantified hypothesis nor to a term.")
+      with Not_found ->
+	(* Interactive mode *)
+	if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+	else ElimOnConstr
+	  (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+	  NoBindings)
 
 let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
 let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
@@ -2735,6 +2755,7 @@ let bad_tactic_args s =
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := Gmap.add kn td !mactab
+let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
 
 type tacdef_kind = | NewTac of identifier
 		   | UpdateTac of ltac_constant
@@ -2749,9 +2770,7 @@ let load_md i ((sp,kn),defs) =
 	  let kn = Names.make_kn mp dir (label_of_id id) in
 	    Nametab.push_tactic (Until i) sp kn;
 	    add (kn,t)
-      | UpdateTac kn ->
-	  mactab := Gmap.remove kn !mactab;
-	  add (kn,t)) defs
+      | UpdateTac kn -> replace (kn,t)) defs
     
 let open_md i((sp,kn),defs) =
   let dp,_ = repr_path sp in
@@ -2762,10 +2781,7 @@ let open_md i((sp,kn),defs) =
 	  let sp = Libnames.make_path dp id in
 	  let kn = Names.make_kn mp dir (label_of_id id) in
 	    Nametab.push_tactic (Exactly i) sp kn
-      | UpdateTac kn -> 
-	  let (path, id) = decode_kn kn in
-	  let sp = Libnames.make_path path id in
-	  Nametab.push_tactic (Exactly i) sp kn) defs
+      | UpdateTac kn -> ()) defs
 
 let cache_md x = load_md 1 x
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index add57cb5..b66bdb85 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacinterp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: tacinterp.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
 (*i*)
 open Dyn
@@ -44,6 +44,9 @@ and interp_sign =
     debug : debug_info;
     trace : ltac_trace }
 
+val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> 
+  Pretyping.var_map * Pretyping.unbound_ltac_var_map
+
 (* Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28e987fa..3db6bcef 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
+(* $Id: tacticals.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Pp
 open Util
@@ -26,7 +26,6 @@ open Clenvtac
 open Rawterm
 open Pattern
 open Matching
-open Evar_refiner
 open Genarg
 open Tacexpr
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c567034..0a8b5d01 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -155,19 +155,37 @@ let order_hyps      = Tacmach.order_hyps
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
 
+(**************************************************************)
+(*          Fresh names                                       *)
+(**************************************************************)
+
+let fresh_id_avoid avoid id =
+  next_global_ident_away true id avoid
+
+let fresh_id avoid id gl =
+  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
+
+(**************************************************************)
+(*          Fixpoints and CoFixpoints                         *)
+(**************************************************************)
+
 (* Refine as a fixpoint *)
 let mutual_fix = Tacmach.mutual_fix
 
-let fix ido n = match ido with
-  | None -> mutual_fix (Pfedit.get_current_proof_name ()) n []
-  | Some id -> mutual_fix id n []
+let fix ido n gl = match ido with
+  | None -> 
+      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
+  | Some id ->
+      mutual_fix id n [] gl
 
 (* Refine as a cofixpoint *)
 let mutual_cofix = Tacmach.mutual_cofix
 
-let cofix = function
-  | None -> mutual_cofix (Pfedit.get_current_proof_name ()) []
-  | Some id -> mutual_cofix id []
+let cofix ido gl = match ido with
+  | None -> 
+      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
+  | Some id ->
+      mutual_cofix id [] gl
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
@@ -286,12 +304,6 @@ let unfold_constr = function
 (*         Introduction tactics            *)
 (*******************************************)
 
-let fresh_id_avoid avoid id =
-  next_global_ident_away true id avoid
-
-let fresh_id avoid id gl =
-  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
-
 let id_of_name_with_default id = function
   | Anonymous -> id
   | Name id   -> id
@@ -565,9 +577,14 @@ let error_uninstantiated_metas t clenv =
   let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
   in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
-let clenv_refine_in with_evars id clenv gl =
+let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let new_hyp_typ  = clenv_type clenv in
+  let clenv = 
+    if with_classes then 
+      { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
+    else clenv
+  in
+  let new_hyp_typ = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf  = clenv_value clenv in
@@ -1098,9 +1115,6 @@ let forward_general_multi_rewrite =
 let register_general_multi_rewrite f =
   forward_general_multi_rewrite := f
 
-let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
-let case_last  = tclLAST_HYP simplest_case
-
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1111,8 +1125,8 @@ let error_unexpected_extra_pattern loc nb pat =
        str (if nb = 1 then "was" else "were") ++
       strbrk " expected in the branch).")
 
-let intro_or_and_pattern loc b ll l' tac =
-  tclLAST_HYP (fun c gl ->
+let intro_or_and_pattern loc b ll l' tac id gl =
+    let c = mkVar id in
     let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
     let nv = mis_constr_nargs ind in
     let bracketed = b or not (l'=[]) in
@@ -1126,10 +1140,10 @@ let intro_or_and_pattern loc b ll l' tac =
     let ll = fix_empty_or_and_pattern (Array.length nv) ll in
     check_or_and_pattern_size loc ll (Array.length nv);
     tclTHENLASTn
-      (tclTHEN case_last clear_last)
+      (tclTHEN (simplest_case c) (clear [id]))
       (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
 	nv (Array.of_list ll))
-      gl)
+      gl
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
@@ -1194,8 +1208,9 @@ let rec intros_patterns b avoid thin destopt = function
   | (loc, IntroOrAndPattern ll) :: l' ->
       tclTHEN
         introf
-        (intro_or_and_pattern loc b ll l'
-	  (intros_patterns b avoid thin destopt))
+        (onLastHyp
+	  (intro_or_and_pattern loc b ll l'
+	    (intros_patterns b avoid thin destopt)))
   | (loc, IntroRewrite l2r) :: l ->
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
@@ -1229,8 +1244,10 @@ let prepare_intros s ipat gl = match ipat with
   | IntroRewrite l2r -> 
       let id = make_id s gl in
       id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
-  | IntroOrAndPattern ll -> make_id s gl, 
-      intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+  | IntroOrAndPattern ll -> make_id s gl,
+      onLastHyp
+	(intro_or_and_pattern loc true ll [] 
+	  (intros_patterns true [] [] no_move))
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -1261,6 +1278,7 @@ let as_tac id ipat = match ipat with
       !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+        id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
       user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
@@ -2167,7 +2185,7 @@ let dependent_pattern c gl =
     let conclvar = subst_term_occ all_occurrences c ty in
       mkNamedLambda id cty conclvar
   in
-  let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+  let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
   let concllda = List.fold_left mklambda (pf_concl gl) subst in 
   let conclapp = applistc concllda (List.rev_map pi1 subst) in
     convert_concl_no_check conclapp DEFAULTcast gl