Better handling of aliases, add command to solve a particular obligation.

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

8 files changed, 57 insertions, 26 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index d38902c963..7e66369f6b 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -142,3 +142,19 @@ Ltac elim_eq_rect :=
 	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
       end
   end.
+
+Ltac real_elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        | context [ @eq_rect _ _ _ _ _ ?p ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+      end
+  end.
+ 
\ No newline at end of file
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index a83a321de0..1d19dbd194 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -42,10 +42,8 @@ Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
-Axiom pair : Type -> Type -> Type.
-Extract Constant pair "'a" "'b" => " 'a * 'b ".
-Extract Inductive prod => "pair" [ "" ].
-Extract Inductive sigT => "pair" [ "" ].
+(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
+(* Extract Inductive sigT => "prod" [ "" ]. *)
 
 Require Export ProofIrrelevance.
 Require Export Coq.subtac.Heq.
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 05334ad760..d6040646e8 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -104,6 +104,13 @@ VERNAC COMMAND EXTEND Subtac_Obligations
 | [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
 END
 
+VERNAC COMMAND EXTEND Subtac_Solve_Obligation
+| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ]
+      END
+
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
     [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 7f71bfa72c..f489325a11 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1612,18 +1612,20 @@ let constr_of_pat env isevars arsign pat avoid =
 	     print_env env ++ str" should have type: " ++ my_print_constr env ty);
     match pat with
     | PatVar (l,name) -> 
+	trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name)));
 	let name, avoid = match name with
 	    Name n -> name, avoid
 	  | Anonymous -> 
 	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
 		Name id, id :: avoid 
 	in
-(* 	  trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *)
+	  trace (str "Treated pattern variable " ++ str (string_of_id (id_of_name name)));
 	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
     | PatCstr (l,((_, i) as cstr),args,alias) ->
-	let _ind = inductive_of_constructor cstr in
+	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in
 	let ind, params = dest_ind_family indf in
+	if ind <> cind then error_bad_constructor_loc l cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
@@ -1694,18 +1696,24 @@ let eq_id avoid id =
 let rels_of_patsign = 
   List.map (fun ((na, b, t) as x) -> 
     match b with 
-      | Some t when kind_of_term t = Rel 0 -> (na, None, t)
+      | Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
       | _ -> x)
 
-let vars_of_ctx = 
-  List.rev_map (fun (na, b, t) -> 
-    match b with 
-      | Some t when kind_of_term t = Rel 0 -> hole
-      | _ ->
-	  match na with
-	      Anonymous -> raise (Invalid_argument "vars_of_ctx")
-	    | Name n -> RVar (dummy_loc, n))
-
+let vars_of_ctx ctx = 
+  let _, y =
+    List.fold_right (fun (na, b, t)  (prev, vars) -> 
+      match b with 
+	| Some t' when kind_of_term t' = Rel 0 -> 
+	    prev, 
+	    (RApp (dummy_loc, 
+		(RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+	| _ ->
+	    match na with
+		Anonymous -> raise (Invalid_argument "vars_of_ctx")
+	      | Name n -> n, RVar (dummy_loc, n) :: vars)
+      ctx (id_of_string "vars_of_ctx: error", [])
+  in List.rev y
+      
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
   | [] -> raise (Invalid_argument "unsafe_fold_right")
@@ -1827,7 +1835,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 	   (* lift to get outside of past patterns to get terms in the combined environment. *)
 	   (fun (pats, n) (sign, c, (s, args), p) ->
 	     let len = List.length sign in
-	       ((sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
+	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
 	   ([], 0) pats 
 	 in
 	 let rhs_rels' = rels_of_patsign rhs_rels in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 3c8fd1d45a..efdcd3e68e 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -113,15 +113,6 @@ let (input,output) =
       export_function = (fun x -> Some x) }
     
 open Evd
-
-let terms_of_evar ev = 
-  match ev.evar_body with
-      Evar_defined b ->
-	let nc = Environ.named_context_of_val ev.evar_hyps in
-	let body = Termops.it_mkNamedLambda_or_LetIn b nc in
-	let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
-	  body, typ
-    | _ -> assert(false)
 	  
 let rec intset_to = function
     -1 -> Intset.empty
@@ -371,6 +362,13 @@ and solve_obligations n tac =
 and solve_all_obligations tac = 
   ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
       
+and try_solve_obligation n prg tac = 
+  let prg = get_prog prg in 
+  let obls, rem = prg.prg_obligations in
+  let obls' = Array.copy obls in
+    if solve_obligation_by_tac prg obls' n tac then
+      ignore(update_obls prg obls' (pred rem));
+    
 and try_solve_obligations n tac = 
   ignore (solve_obligations n tac)
 
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 8a64551369..30f4998463 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -21,6 +21,8 @@ val solve_obligations : Names.identifier option -> Proof_type.tactic -> int
 
 val solve_all_obligations : Proof_type.tactic -> unit 
 
+val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit
+
 val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 5d8158e863..9a11f60b3e 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -32,6 +32,7 @@ let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
 let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
 let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
 
 let make_ref s = Qualid (dummy_loc, qualid_of_string s)
 let sig_ref = make_ref "Init.Specif.sig"
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 07be96090b..a87bbfbeda 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -27,6 +27,7 @@ val fix_sub_ref : global_reference lazy_t
 val fix_measure_sub_ref : global_reference lazy_t
 val lt_ref : global_reference lazy_t
 val lt_wf_ref : global_reference lazy_t
+val refl_ref : global_reference lazy_t
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference