factorisation et generalisation des clauses

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

3 files changed, 22 insertions, 10 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0019b86010..efbf675b7b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -138,7 +138,7 @@ let instantiate n c ido gl =
   let evl = 
     match ido with
 	None -> evars_of wc.sigma gl.it.evar_concl 
-      | Some id -> 
+      | Some (id,_,_) -> 
 	  let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in
 	    evars_of wc.sigma typ in
     if List.length evl < n then error "not enough evars";
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 0ee86be935..d5f11b6d4b 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +50,7 @@ val w_conv_x            : wc -> constr -> constr -> bool
 val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
-val instantiate : int -> constr -> identifier option -> tactic
+val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f1c5763289..21c2d0c400 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -56,7 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *)
   | InHypValueOnly
 
 type 'a raw_hyp_location = 
-    'a * (hyp_location_flag * hyp_location_flag option ref)
+    'a * int list * (hyp_location_flag * hyp_location_flag option ref)
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
@@ -70,8 +70,6 @@ type intro_pattern_expr =
 
 and case_intro_pattern_expr = intro_pattern_expr list list
 
-type 'id clause_pattern = int list option * ('id * int list) list
-
 type inversion_kind =
   | SimpleInversion
   | FullInversion
@@ -84,6 +82,20 @@ type ('c,'id) inversion_strength =
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
 
+type 'id gsimple_clause = ('id raw_hyp_location) option
+(* onhyps:
+     [None] means *on every hypothesis*
+     [Some l] means on hypothesis belonging to l *)
+type 'id gclause =
+  { onhyps : 'id raw_hyp_location list option;
+    onconcl : bool;
+    concl_occs :int list }
+
+let simple_clause_of = function
+    { onhyps = Some[scl]; onconcl = false } -> Some scl
+  | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
+  | _ -> error "not a simple clause (one hypothesis or conclusion)"
+
 type pattern_expr = constr_expr
 
 (* Type of patterns *)
@@ -121,8 +133,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacForward of bool * name * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of identifier * 'constr * 'id clause_pattern
-  | TacInstantiate of int * 'constr * 'id option
+  | TacLetTac of identifier * 'constr * 'id gclause
+  | TacInstantiate of int * 'constr * 'id gclause
 
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
@@ -162,13 +174,13 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacConstructor of int or_metaid * 'constr bindings
 
   (* Conversion *)
-  | TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list
+  | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
   | TacChange of
-      'constr occurrences option * 'constr * 'id raw_hyp_location list
+      'constr occurrences option * 'constr * 'id gclause
 
   (* Equivalence relations *)
   | TacReflexivity
-  | TacSymmetry of 'id option
+  | TacSymmetry of 'id gclause
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)