Opacity parameterization for obligations working.

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

5 files changed, 34 insertions, 17 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index 8c8f7c43a..1d4d948ac 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -74,10 +74,15 @@ Ltac bang :=
       end
   end.
 
+Require Import Eqdep.
+
 Ltac elim_eq_rect :=
   match goal with
-    | [ |- ?t ] => 
-      match t with
-        context [ @eq_rect _ _ _ _ _ ?p ] => try case p ; simpl
-      end
+  | [ |- ?t ] => 
+    match t with
+    context [ @eq_rect _ _ _ _ _ ?p ] => 
+      let t := fresh "t" in 
+      set (t := p); simpl in t ; 
+	try ((case t ; clear t) || (clearbody t; rewrite (UIP_refl _ _ t); clear t))
+    end
   end.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 33b140f61..e0711cade 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -65,8 +65,8 @@ let subst_evar_constr evs n t =
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
 	let args = 
-	  let (l, r) = list_split_at chop (Array.to_list args) in
-	    r
+	  let (l, r) = list_split_at chop (List.rev (Array.to_list args)) in
+	    List.rev r
 	in
 	let args =
 	  let rec aux hyps args acc =
@@ -179,7 +179,7 @@ let eterm_obligations name nclen evm fs t tycon =
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, _, typ, deps)) -> name, typ, deps) evts
+    List.map (fun (_, ((_, name), _, chop, typ, deps)) -> name, typ, chop = fs, deps) evts
   in
     (try
        trace (str "Term given to eterm" ++ spc () ++
@@ -187,7 +187,7 @@ let eterm_obligations name nclen evm fs t tycon =
        trace (str "Term constructed in eterm" ++ spc () ++
 		Termops.print_constr_env (Global.env ()) t');
        ignore(iter
-		(fun (name, typ, deps) ->
+		(fun (name, typ, _, deps) ->
 		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
 			    Termops.print_constr_env (Global.env ()) typ))
 		evars);
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a7fcecf2a..a67020c52 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -20,6 +20,7 @@ val mkMetas : int -> constr list
 
 val eterm_obligations : identifier -> int -> evar_map -> int -> constr -> types option -> (* id, named context length, evars, number of
 											     function prototypes to try to clear from evars contexts *)
-  (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *)
+  (identifier * types * bool * Intset.t) array * constr
+    (* Obl. name, type as product, chopping of products flag, and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 85c937cf2..a7bb53c59 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,12 +12,13 @@ open Decl_kinds
 open Util
 open Evd
 
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
 
 type obligation =
     { obl_name : identifier;
       obl_type : types;
       obl_body : constr option;
+      obl_opaque : bool;
       obl_deps : Intset.t;
     }
 
@@ -114,7 +115,8 @@ let subst_body prg =
 let declare_definition prg =
   let body = subst_body prg in
     (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
-		  my_print_constr (Global.env()) body);
+		  my_print_constr (Global.env()) body ++ str " : " ++ 
+		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
   let ce = 
     { const_entry_body = body;
@@ -164,7 +166,7 @@ let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
       const_entry_type = Some obl.obl_type;
-      const_entry_opaque = false;
+      const_entry_opaque = obl.obl_opaque;
       const_entry_boxed = false} 
   in
   let constant = Declare.declare_constant obl.obl_name 
@@ -191,10 +193,10 @@ let red = Reductionops.nf_betaiota
 let init_prog_info n b t deps nvrec obls =
   let obls' = 
     Array.mapi
-      (fun i (n, t, d) ->
+      (fun i (n, t, o, d) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; 
-	   obl_type = red t; 
+	   obl_type = red t; obl_opaque = o;
 	   obl_deps = d })
       obls
   in
@@ -247,6 +249,10 @@ let deps_remaining obls deps =
 	 else x :: acc)
       deps []
 
+let kind_of_opacity o =
+  if o then Subtac_utils.goal_proof_kind
+  else Subtac_utils.goal_kind
+
 let solve_obligation prg num =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
@@ -257,7 +263,7 @@ let solve_obligation prg num =
       match deps_remaining obls obl.obl_deps with
 	  [] ->
 	    let obl = subst_deps_obl obls obl in
-	      Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
+	      Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
 		(fun strength gr -> 
 		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
@@ -290,6 +296,7 @@ let obligations_of_evars evars =
 	    { obl_name = n;
 	      obl_type = t;
 	      obl_body = None;
+	      obl_opaque = false;
 	      obl_deps = Intset.empty;
 	    }) evars)
   in arr, Array.length arr
@@ -303,7 +310,10 @@ let solve_obligation_by_tac prg obls i tac =
 	   if deps_remaining obls obl.obl_deps = [] then
 	     let obl = subst_deps_obl obls obl in
 	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	       obls.(i) <- { obl with obl_body = Some t };
+	       if obl.obl_opaque then 
+		 obls.(i) <- declare_obligation obl t
+	       else
+		 obls.(i) <- { obl with obl_body = Some t };
 	       true		 
 	   else false
 	 with _ -> false)  
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index ff6163b5b..28444e4c9 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,6 +1,7 @@
 open Util
 
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
+    (* ident, type, opaque or transparent, dependencies *)
 
 val set_default_tactic : Tacexpr.glob_tactic_expr -> unit