Imported Upstream version 8.3.pl3upstream/8.3.pl3

6 files changed, 85 insertions, 15 deletions

diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index b29b8362..763ed82f 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e47f19bf..41fafdf1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 84470a0f..aa42f6cd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -504,6 +504,15 @@ and intros_with_rewrite_aux : tactic =
 				     intros_with_rewrite
 				   ]
 			  g
+		      else if isVar args.(2) 
+		      then 
+			let id = pf_get_new_id (id_of_string "y") g  in
+			tclTHENSEQ [ h_intro id;
+				     generalize_dependent_of (destVar args.(2)) id;
+				     tclTRY (Equality.rewriteRL (mkVar id));
+				     intros_with_rewrite
+				   ]
+			  g
 		      else
 			begin
 			  let id = pf_get_new_id (id_of_string "y") g  in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 799180b7..40ee116d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 3c3a36f0..b74422a3 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -716,11 +716,11 @@ and build_entry_lc_from_case env funname make_discr
 	*)
 	let case_resl =
 	    List.fold_right
-	    (fun (case_arg,_) ctxt_argsl ->
-	       let arg_res = build_entry_lc env funname avoid case_arg  in
-	       combine_results combine_args arg_res ctxt_argsl
-	    )
-	    el
+	      (fun (case_arg,_) ctxt_argsl ->
+		let arg_res = build_entry_lc env funname avoid case_arg  in
+		combine_results combine_args arg_res ctxt_argsl
+	      )
+	      el
 	      (mk_result [] [] avoid)
 	in
 	let types =
@@ -876,6 +876,32 @@ let is_res id =
   with Invalid_argument _ -> false
 
 
+
+let same_raw_term rt1 rt2 = 
+  match rt1,rt2 with 
+    | RRef(_,r1), RRef (_,r2) -> r1=r2
+    | RHole _, RHole _ -> true
+    | _ -> false
+let decompose_raw_eq lhs rhs = 
+  let rec decompose_raw_eq lhs rhs acc = 
+    observe (str "decomposing eq for " ++ pr_rawconstr lhs ++ str " " ++ pr_rawconstr rhs);
+    let (rhd,lrhs) = raw_decompose_app rhs in 
+    let (lhd,llhs) = raw_decompose_app lhs in 
+    observe (str "lhd := " ++ pr_rawconstr lhd);
+    observe (str "rhd := " ++ pr_rawconstr rhd);
+    observe (str "llhs := " ++ int (List.length llhs));
+    observe (str "lrhs := " ++ int (List.length lrhs));
+    let sllhs = List.length llhs in 
+    let slrhs = List.length lrhs in 
+    if same_raw_term lhd rhd && sllhs = slrhs 
+    then
+      (* let _ = assert false in  *)
+      List.fold_right2 decompose_raw_eq	llhs lrhs acc
+    else (lhs,rhs)::acc
+  in
+  decompose_raw_eq lhs rhs []
+     
+
 exception Continue
 (*
    The second phase which reconstruct the real type of the constructor.
@@ -1032,6 +1058,41 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     mkRProd(n,t,new_b),id_to_exclude
 		     else new_b, Idset.add id id_to_exclude
 		  *)
+	    | RApp(loc1,RRef(loc2,eq_as_ref),[ty;rt1;rt2])
+		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
+		  ->
+	      begin
+		try 
+		  let l = decompose_raw_eq rt1 rt2 in 
+		  if List.length l > 1 
+		  then 
+		    let new_rt =
+		      List.fold_left 
+			(fun acc (lhs,rhs) -> 
+			  mkRProd(Anonymous,
+				  mkRApp(mkRRef(eq_as_ref),[mkRHole ();lhs;rhs]),acc)
+			)
+			b
+			l
+		    in
+		    rebuild_cons env nb_args relname args crossed_types depth new_rt
+		  else raise Continue
+	      with Continue -> 
+		observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+		let t' = Pretyping.Default.understand Evd.empty env t in
+		let new_env = Environ.push_rel (n,None,t') env in
+		let new_b,id_to_exclude =
+		  rebuild_cons new_env
+		    nb_args relname
+		    args new_crossed_types
+		    (depth + 1) b
+		in
+		match n with
+		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Idset.remove id
+			(Idset.filter not_free_in_t id_to_exclude)
+		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_rawconstr rt);
 		let t' = Pretyping.Default.understand Evd.empty env t in
@@ -1122,12 +1183,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 
 (* debuging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
-(*   observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++  *)
-(* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
+  observe  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
+		 str "nb_args := " ++ str (string_of_int nb_args));
   let res =
     rebuild_cons env nb_args relname args crossed_types 0 rt
   in
-(*   observe (str " leads to "++ pr_rawconstr (fst res)); *)
+  observe (str " leads to "++ pr_rawconstr (fst res));
   res
 
 
@@ -1266,7 +1327,7 @@ let do_build_inductive
       (function result (* (args',concl') *) ->
 	 let rt = compose_raw_context result.context result.value in
 	 let nb_args = List.length funsargs.(i) in
-	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
+	  (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
 	 fst (
 	   rebuild_cons env_with_graphs nb_args relnames.(i)
 	     []
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9c4cc78a..83868da9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Term
 open Termops