fixed czar bug with parametric inductives

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

4 files changed, 47 insertions, 23 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 77357e3fa..bfb5039d5 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -327,9 +327,9 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let _ =
     let expected = mib.Declarations.mind_nparams - num_params in
       if List.length params <> expected then
-	errorlabstrm "suppose it is"
-	  (str "Wrong number of extra arguments: " ++
-	     (if expected = 0 then str "none" else int expected) ++
+	errorlabstrm "suppose it is" 
+	  (str "Wrong number of extra arguments: " ++ 
+	     (if expected = 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
     let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index c2a32471e..bde403657 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -1151,9 +1151,9 @@ let case_tac params pat_info hyps gls0 =
       | _ -> anomaly "wrong place for cases" in
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
-  let nek =
-    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info
-      pat_info.pat_pat ek in
+  let nek = 
+    register_dep_subcase (id,(List.length params,List.length hyps)) 
+      (pf_env gls0) per_info pat_info.pat_pat ek in  
   let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
     tclTHENS (assert_postpone id clause)
       [tclTHENLIST
@@ -1216,6 +1216,7 @@ let hrec_for fix_id per_info gls obj_id =
   let hd2 = applist (mkVar fix_id,args@[obj]) in
     compose_lam rc (whd_beta gls.sigma hd2)
 
+
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
       Close_patt t,_ ->
@@ -1224,16 +1225,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | Skip_patt (_,t),skipped::next_objs ->
 	let args0 = push_arg skipped args in
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
-    | End_patt (id,nhyps),[] ->
+    | End_patt (id,(nparams,nhyps)),[] -> 
 	begin
 	  match List.assoc id args with
-	      [None,br_args] ->
-		let metas =
-		  list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+	      [None,br_args] -> 
+		let all_metas = 
+		  list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		let param_metas,hyp_metas = list_chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
-		    (tacnext
-		       (applist (mkVar id,List.rev_append br_args metas))) gls
+		    (tacnext 
+		       (applist (mkVar id,
+				 List.append param_metas 
+				   (List.rev_append br_args hyp_metas)))) gls
 	    | _ -> anomaly "wrong stack size"
 	end
     | Split_patt (ids,ind,br), casee::next_objs ->
@@ -1307,7 +1311,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | End_patt (_,_) , _ :: _  ->
 	anomaly "execute_cases : End of branch with garbage left"
 
-
+let understand_my_constr c gls =
+  let env = pf_env gls in
+  let nc = names_of_rel_context env in
+  let rawc = Detyping.detype false [] nc c in
+  let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc ->  map_rawconstr frob rc in
+    Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+
+let set_refine,my_refine =
+let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
+((fun tac -> refine:= tac),
+(fun c gls -> 
+   let oc = understand_my_constr c gls in
+     !refine oc gls))
 
 (* end focus/claim *)
 
@@ -1348,9 +1364,9 @@ let end_tac et2 gls =
 		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
-		 execute_cases Anonymous pi
-		   (fun c -> tclTHENLIST
-		      [refine c;
+		 execute_cases Anonymous pi 
+		   (fun c -> tclTHENLIST 
+		      [my_refine c;
 		       clear clauses;
 		       justification assumption])
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
@@ -1371,7 +1387,7 @@ let end_tac et2 gls =
 			     (fun c ->
 				tclTHENLIST
 				  [clear [fix_id];
-				   refine c;
+				   my_refine c;
 				   clear clauses;
 				   justification assumption])
 			     (initial_instance_stack clauses)
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index a05c36e93..ada5e7448 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -42,21 +42,21 @@ val execute_cases :
     (Names.Idset.elt * (Term.constr option * Term.constr list) list) list ->
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
-val tree_of_pats :
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+val tree_of_pats : 
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree
 
-val add_branch :
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+val add_branch : 
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val append_branch :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   (Names.Idset.t * Decl_mode.split_tree) option ->
   (Names.Idset.t * Decl_mode.split_tree) option
 
 val append_tree :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val build_dep_clause :   Term.types Decl_expr.statement list ->
@@ -65,8 +65,13 @@ val build_dep_clause :   Term.types Decl_expr.statement list ->
     (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis)
     Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
 
+<<<<<<< HEAD:tactics/decl_proof_instr.mli
 val register_dep_subcase :
     Names.identifier * int ->
+=======
+val register_dep_subcase :    
+    Names.identifier * (int * int) ->
+>>>>>>> ada3fb4... fixed czar bug with parametric inductives:tactics/decl_proof_instr.mli
     Environ.env ->
     Decl_mode.per_info ->
     Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -116,3 +121,4 @@ val init_tree:
      (Names.Idset.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
 
+val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 5258b319b..fe81dadce 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -379,3 +379,5 @@ let refine (evd,c) gl =
      complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) evd c in
   tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
+
+let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *)