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

8 files changed, 149 insertions, 85 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index f341580e..87a47200 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -346,7 +346,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) -> 
 	   RVar (loc,id)) params in 
     let dum_args= 
-      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark))
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false))
 	oib.Declarations.mind_nrealargs in
       raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
@@ -369,7 +369,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term2 =
     RLetIn(dummy_loc,Anonymous,
 	   RCast(dummy_loc,raw_of_pat npatt,
-		 CastConv DEFAULTcast,app_ind),term1) in
+		 CastConv (DEFAULTcast,app_ind)),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in  
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index b19d8c04..a34446d8 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -886,11 +886,11 @@ let build_per_info etype casee gls =
 	 ET_Induction -> mind.mind_nparams_rec
        | _ -> mind.mind_nparams in
   let params,real_args = list_chop nparams args in
-  let abstract_obj body c = 
+  let abstract_obj c body = 
     let typ=pf_type_of gls c in 
       lambda_create env (typ,subst_term c body) in
-  let pred= List.fold_left abstract_obj    
-    (lambda_create env (ctyp,subst_term casee concl)) real_args in
+  let pred= List.fold_right abstract_obj    
+    real_args (lambda_create env (ctyp,subst_term casee concl)) in
     is_dep,
   {per_casee=casee;
    per_ctype=ctyp;
@@ -1273,7 +1273,7 @@ end*)
 
 
 let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
-  match tree with
+	      match tree with
       Pop t ->  
 	let is_rec,nstacks =  pop_stacks stacks in
 	  if is_rec then
@@ -1309,51 +1309,59 @@ let rec execute_cases at_top fix_name per_info kont0 stacks tree gls =
 				    kont] gls)
 	    end gls
     | Split(ids,ind,br) ->
-	let (_,typ,_)=destProd (pf_concl gls) in
+	let (_,typ,_)= 
+	  try destProd (pf_concl gls) with Invalid_argument _ ->
+  	    anomaly "Sub-object not found." in
 	let hd,args=decompose_app (special_whd gls typ) in
-	let _ = assert (ind = destInd hd) in
-	let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
-	let params = list_firstn nparams args in
-	let constr i =applist (mkConstruct(ind,succ i),params) in
-	let next_tac is_rec i = function
-	    Some (sub_ids,tree) ->
-	      let br_stacks =
-		List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in
-	      let p_stacks = 
-		push_head (constr i) is_rec ids br_stacks in
-		execute_cases false fix_name per_info kont0 p_stacks tree 
-	  | None -> 
-	      msgnl (str "Warning : missing case");
-	      kont0 (mkMeta 1) 
-	in
-	let id = pf_get_new_id patvar_base gls in
-	let kont is_rec = 			
-	  tclTHENSV
-	    (general_case_analysis (mkVar id,NoBindings))
-	    (Array.mapi (next_tac is_rec) br) in
-	  tclTHEN 
-	    (intro_mustbe_force id)
-	    begin
-	      match fix_name with
-		  Anonymous -> kont false
-		| Name fix_id ->  
-		    (fun gls -> 
-		       if at_top then
-			 kont false gls
-		       else
-			 match hrec_for id fix_id per_info gls with
-			     None -> kont false gls
-			   | Some c_obj ->
-			       tclTHENLIST 
-				 [generalize [c_obj];
-				  kont true] gls)
-	    end gls
+	  if try ind <> destInd hd with Invalid_argument _ -> true then
+	      (* argument of an inductive family : intro + discard *)
+	      tclTHEN intro
+  		(execute_cases at_top fix_name per_info kont0 stacks tree) gls
+	    else
+	      begin
+		let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+		let params = list_firstn nparams args in
+		let constr i =applist (mkConstruct(ind,succ i),params) in
+		let next_tac is_rec i = function
+		    Some (sub_ids,tree) ->
+		      let br_stacks =
+			List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in
+		      let p_stacks = 
+			push_head (constr i) is_rec ids br_stacks in
+			execute_cases false fix_name per_info kont0 p_stacks tree 
+		  | None -> 
+		      msgnl (str "Warning : missing case");
+		      kont0 (mkMeta 1) 
+		in
+		let id = pf_get_new_id patvar_base gls in
+		let kont is_rec = 			
+		  tclTHENSV
+		    (general_case_analysis (mkVar id,NoBindings))
+		    (Array.mapi (next_tac is_rec) br) in
+		  tclTHEN 
+		    (intro_mustbe_force id)
+		    begin
+		      match fix_name with
+			  Anonymous -> kont false
+			| Name fix_id ->  
+			    (fun gls -> 
+			      if at_top then
+				kont false gls
+			    else
+				match hrec_for id fix_id per_info gls with
+				    None -> kont false gls
+				  | Some c_obj ->
+				      tclTHENLIST 
+					[generalize [c_obj];
+					 kont true] gls)
+		    end gls
+	      end
     | End_of_branch (id,nhyps) -> 
-	  match List.assoc id stacks with
-	      [None,_,args] -> 
-		let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in
-		  kont0 (applist (mkVar id,List.rev_append args metas)) gls
-	    | _ -> anomaly "wrong stack size"
+	match List.assoc id stacks with
+	    [None,_,args] -> 
+	      let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		kont0 (applist (mkVar id,List.rev_append args metas)) gls
+	  | _ -> anomaly "wrong stack size"
 
 let end_tac et2 gls =
   let info = get_its_info gls in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 754aec1c..24a7e34e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 9521 2007-01-23 14:31:21Z notin $ *)
+(* $Id: equality.ml 9835 2007-05-17 22:23:03Z jforest $ *)
 
 open Pp
 open Util
@@ -93,7 +93,7 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
       (* Original code. In particular, [splay_prod] performs delta-reduction. *)
       let env = pf_env gl in
       let sigma = project gl in 
-      let _,t = splay_prod env sigma t in
+      let _,t = splay_prod env sigma ctype in
 	match match_with_equation t with
 	  | None -> 
 	      if l = NoBindings
@@ -313,6 +313,13 @@ let discriminable env sigma t1 t2 =
     | Inl _ -> true
     | _ -> false
 
+let injectable env sigma t1 t2 = 
+    match find_positions env sigma t1 t2 with
+    | Inl _ | Inr [] -> false
+    | Inr _ -> true
+
+
+
 (* Once we have found a position, we need to project down to it.  If
    we are discriminating, then we need to produce False on one of the
    branches of the discriminator, and True on the other one.  So the
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3d6a08b6..93cf53bd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: equality.mli 9195 2006-10-01 09:41:57Z herbelin $ i*)
+(*i $Id: equality.mli 9835 2007-05-17 22:23:03Z jforest $ i*)
 
 (*i*)
 open Names
@@ -105,6 +105,7 @@ val substHyp : bool -> types -> identifier -> tactic
 *)
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 2727e669..c14462eb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: setoid_replace.ml 9331 2006-11-01 09:36:06Z herbelin $ *)
+(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
 
 open Tacmach
 open Proof_type
@@ -709,9 +709,10 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
 let unify_relation_carrier_with_type env rel t =
  let raise_error quantifiers_no =
   errorlabstrm "New Morphism"
-   (str "One morphism argument or its output has type " ++ pr_lconstr t ++
+   (str "One morphism argument or its output has type " ++ 
+    pr_lconstr_env env t ++
     str " but the signature requires an argument of type \"" ++
-    pr_lconstr rel.rel_a ++ str " " ++ prvect_with_sep pr_spc (fun _ -> str  "?")
+    pr_lconstr_env env rel.rel_a ++ prvect_with_sep mt (fun _ -> str " ?")
      (Array.make quantifiers_no 0) ++ str "\"") in
  let args =
   match kind_of_term t with
@@ -757,9 +758,10 @@ let unify_relation_class_carrier_with_type env rel t =
       rel
      else
       errorlabstrm "New Morphism"
-       (str "One morphism argument or its output has type " ++ pr_lconstr t ++
+       (str "One morphism argument or its output has type " ++ 
+        pr_lconstr_env env t ++
         str " but the signature requires an argument of type " ++
-        pr_lconstr t')
+        pr_lconstr_env env t')
   | Leibniz None -> Leibniz (Some t)
   | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
 
@@ -961,6 +963,8 @@ let new_named_morphism id m sign =
   match sign with
      None -> None
    | Some (args,out) ->
+      if args = [] then
+	error "Morphism signature expects at least one argument.";
       Some
        (List.map (fun (variance,ty) -> variance, constr_of ty) args,
         constr_of out)
@@ -1947,7 +1951,7 @@ let setoid_reflexivity gl =
            (str "The relation " ++ prrelation rel ++ str " is not reflexive.")
        | Some refl -> apply refl gl
  with
-  Optimize -> reflexivity gl
+  Optimize -> reflexivity_red true gl
 
 let setoid_symmetry gl =
  try
@@ -1963,7 +1967,7 @@ let setoid_symmetry gl =
            (str "The relation " ++ prrelation rel ++ str " is not symmetric.")
        | Some sym -> apply sym gl
  with
-  Optimize -> symmetry gl
+  Optimize -> symmetry_red true gl
 
 let setoid_symmetry_in id gl =
  let new_hyp =
@@ -1998,7 +2002,7 @@ let setoid_transitivity c gl =
             apply_with_bindings
              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
  with
-  Optimize -> transitivity c gl
+  Optimize -> transitivity_red true c gl
 ;;
 
 Tactics.register_setoid_reflexivity setoid_reflexivity;;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 29150c27..ac6a396f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 9551 2007-01-29 15:13:35Z bgregoir $ *)
+(* $Id: tacinterp.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Constrintern
 open Closure
@@ -1195,7 +1195,7 @@ let interp_hyp_location ist gl ((occs,id),hl) =
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
   { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
     onconcl=b;
-    concl_occs=occs }
+    concl_occs=interp_int_or_var_list ist occs }
 
 (* Interpretation of constructions *)
 
@@ -1253,7 +1253,7 @@ open Evd
 
 let solvable_by_tactic env evi (ev,args) src = 
   match (!implicit_tactic, src) with
-  | Some tac, (ImplicitArg _ | QuestionMark)
+  | Some tac, (ImplicitArg _ | QuestionMark _)
       when 
 	Environ.named_context_of_val evi.evar_hyps = 
 	Environ.named_context env ->
@@ -1827,6 +1827,8 @@ and interp_genarg ist gl x =
         (interp_bindings ist gl (out_gen globwit_bindings x))
   | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x
   | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x
+  | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x
+  | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x
   | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
   | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
   | OptArgType _ -> app_opt (interp_genarg ist gl) x
@@ -1849,6 +1851,16 @@ and interp_genarg_constr_list1 ist gl x =
   let lc = pf_interp_constr_list ist gl lc in
   in_gen (wit_list1 wit_constr) lc
 
+and interp_genarg_var_list0 ist gl x =
+  let lc = out_gen (wit_list0 globwit_var) x in
+  let lc = interp_hyp_list ist gl lc in
+  in_gen (wit_list0 wit_var) lc
+
+and interp_genarg_var_list1 ist gl x =
+  let lc = out_gen (wit_list1 globwit_var) x in
+  let lc = interp_hyp_list ist gl lc in
+  in_gen (wit_list1 wit_var) lc
+
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
   let rec apply_match_subterm ist nocc (id,c) csr mt =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb98ec18..c863a453 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 9605 2007-02-07 12:19:19Z notin $ *)
+(* $Id: tactics.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
 
 open Pp
 open Util
@@ -503,6 +503,20 @@ let cut_in_parallel l =
   in 
     prec (List.rev l)
 
+let error_uninstantiated_metas t clenv =
+  let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in
+  let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
+  in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
+
+let clenv_refine_in id clenv gl =
+  let new_hyp_typ  = clenv_type clenv in
+  if occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv;
+  let new_hyp_prf  = clenv_value clenv in
+  tclTHEN
+    (tclEVARS (evars_of clenv.env))
+    (cut_replacing id new_hyp_typ
+      (fun x gl -> refine_no_check new_hyp_prf gl)) gl
+
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
@@ -575,12 +589,7 @@ let apply_in id lemmas gls =
   let t' = pf_get_hyp_typ gls id in
   let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
   let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
-  let new_hyp_prf  = clenv_value clause in
-  let new_hyp_typ  = clenv_type clause in
-  tclTHEN
-    (tclEVARS (evars_of clause.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+  clenv_refine_in id clause gls
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -839,15 +848,11 @@ let elimination_in_clause_scheme id elimclause indclause gl =
   let hyp_typ = pf_type_of gl hyp in
   let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
-  let new_hyp_prf  = clenv_value elimclause'' in
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
-  tclTHEN
-    (tclEVARS (evars_of elimclause''.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gl
+  clenv_refine_in id elimclause'' gl
 
 let general_elim_in id =
   general_elim_clause (elimination_in_clause_scheme id)
@@ -2328,10 +2333,18 @@ let dImp cls =
 let setoid_reflexivity = ref (fun _ -> assert false)
 let register_setoid_reflexivity f = setoid_reflexivity := f
 
-let reflexivity gl =
-  match match_with_equation (pf_concl gl) with
+let reflexivity_red allowred gl =
+  (* PL: usual reflexivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_reflexivity gl
-    | Some (hdcncl,args) ->  one_constructor 1 NoBindings gl
+    | Some _ -> one_constructor 1 NoBindings gl
+
+let reflexivity gl = reflexivity_red false gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -2345,8 +2358,14 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
 let setoid_symmetry = ref (fun _ -> assert false)
 let register_setoid_symmetry f = setoid_symmetry := f
 
-let symmetry gl =
-  match match_with_equation (pf_concl gl) with
+let symmetry_red allowred gl =
+  (* PL: usual symmetry don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_symmetry gl
     | Some (hdcncl,args) ->
         let hdcncls = string_of_inductive hdcncl in
@@ -2360,7 +2379,7 @@ let symmetry gl =
               | [c1;c2]     -> mkApp (hdcncl, [| c2; c1 |])
 	      | _ -> assert false 
 	    in 
-	    tclTHENLAST (cut symc)
+	    tclTHENFIRST (cut symc)
               (tclTHENLIST 
 		[ intro;
 		  tclLAST_HYP simplest_case;
@@ -2368,6 +2387,8 @@ let symmetry gl =
 	      gl
 	end
 
+let symmetry gl = symmetry_red false gl
+
 let setoid_symmetry_in = ref (fun _ _ -> assert false)
 let register_setoid_symmetry_in f = setoid_symmetry_in := f
 
@@ -2408,8 +2429,14 @@ let intros_symmetry =
 let setoid_transitivity = ref (fun _ _ -> assert false)
 let register_setoid_transitivity f = setoid_transitivity := f
 
-let transitivity t gl =
-  match match_with_equation (pf_concl gl) with
+let transitivity_red allowred t gl =
+  (* PL: usual transitivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_transitivity t gl
     | Some (hdcncl,args) -> 
         let hdcncls = string_of_inductive hdcncl in
@@ -2436,7 +2463,9 @@ let transitivity t gl =
 		    tclLAST_HYP simplest_case;
 		    assumption ])) gl
         end 
-	
+
+let transitivity t gl = transitivity_red false t gl
+
 let intros_transitivity  n  = tclTHEN intros (transitivity n)
 
 (* tactical to save as name a subproof such that the generalisation of 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index aece3231..bb71afb9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactics.mli 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: tactics.mli 9853 2007-05-23 14:25:47Z letouzey $ i*)
 
 (*i*)
 open Names
@@ -276,16 +276,19 @@ val simplest_split             : tactic
 (*s Logical connective tactics. *)
 
 val register_setoid_reflexivity : tactic -> unit
+val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
 val register_setoid_symmetry : tactic -> unit
+val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
 val register_setoid_symmetry_in : (identifier -> tactic) -> unit
 val symmetry_in                 : identifier -> tactic
 val intros_symmetry             : clause -> tactic
 
 val register_setoid_transitivity : (constr -> tactic) -> unit
+val transitivity_red            : bool -> constr -> tactic
 val transitivity                : constr -> tactic
 val intros_transitivity         : constr -> tactic