Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

7 files changed, 33 insertions, 22 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 4ee8001c..7a23d052 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
+(* $Id: evar_refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Util
 open Names
@@ -25,7 +25,7 @@ open Refiner
 let w_refine env ev rawc evd =
   if Evd.is_defined (evars_of evd) ev then 
     error "Instantiate called on already-defined evar";
-  let e_info = Evd.map (evars_of evd) ev in
+  let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
     Pretyping.Default.understand_tcc (evars_of evd) env 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 1f79d73c..ffbc0d56 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 8696 2006-04-11 07:05:50Z herbelin $ *)
+(* $Id: logic.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Pp
 open Util
@@ -285,7 +285,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let (acc'',conclty') =
@@ -327,7 +327,7 @@ and mk_hdgoals sigma goal goalacc trm =
     | App (f,l) ->
 	let (acc',hdty) = 
 	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8b3b5f5f..eb47fc2e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: redexpr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -93,19 +93,26 @@ let declare_red_expr s f =
   with Not_found ->
     red_expr_tab := Stringmap.add s f !red_expr_tab
 
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
+
+let out_with_occurrences (l,c) =
+  (List.map out_arg l, c)
+
 let reduction_of_red_expr = function
   | Red internal -> 
       if internal then (try_red_product,DEFAULTcast) 
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
-  | Simpl (Some (_,c as lp)) -> 
-      (contextually (is_reference c) lp nf,DEFAULTcast)
+  | Simpl (Some (_,c as lp)) ->
+      (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast)
   | Simpl None -> (nf,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
-  | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast)
+  | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
   | Fold cl -> (fold_commands cl,DEFAULTcast)
-  | Pattern lp -> (pattern_occs lp,DEFAULTcast)
+  | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
       (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index c442b16e..cbac180a 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: redexpr.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: redexpr.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
 
 open Names
 open Term
@@ -17,6 +17,8 @@ open Reductionops
 
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
+val out_with_occurrences : 'a with_occurrences -> int list * 'a
+
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 (* [true] if we should use the vm to verify the reduction *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 2b878d37..067ae471 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 8708 2006-04-14 08:13:02Z jforest $ *)
+(* $Id: refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Pp
 open Util
@@ -263,7 +263,7 @@ let extract_open_proof sigma pf =
     let meta_cnt = ref 0 in
     let rec f () =
       incr meta_cnt; 
-      if in_dom sigma (existential_of_int !meta_cnt) then f ()
+      if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
       else !meta_cnt
     in f
   in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index aff6b944..b721dacd 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacexpr.ml 8651 2006-03-21 21:54:43Z jforest $ i*)
+(*i $Id: tacexpr.ml 8917 2006-06-07 16:59:05Z herbelin $ i*)
 
 open Names
 open Topconstr
@@ -56,7 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *)
   | InHypTypeOnly
   | InHypValueOnly
 
-type 'a raw_hyp_location = 'a * int list * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
@@ -80,6 +80,7 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
+
 type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
@@ -87,7 +88,7 @@ type 'id gsimple_clause = ('id raw_hyp_location) option
 type 'id gclause =
   { onhyps : 'id raw_hyp_location list option;
     onconcl : bool;
-    concl_occs :int list }
+    concl_occs : int or_var list }
 
 let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
 
@@ -175,8 +176,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
-  | TacChange of
-      'constr occurrences option * 'constr * 'id gclause
+  | TacChange of 'constr with_occurrences option * 'constr * 'id gclause
 
   (* Equivalence relations *)
   | TacReflexivity
@@ -184,6 +184,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
+  | TacRewrite of bool * 'constr with_bindings * 'id gclause
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
@@ -306,10 +307,10 @@ type closed_raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
 type 'a raw_abstract_argument_type =
-    ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+    ('a,rlevel,raw_tactic_expr) abstract_argument_type
 
 type 'a glob_abstract_argument_type =
-    ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+    ('a,glevel,glob_tactic_expr) abstract_argument_type
 
 type open_generic_argument =
     (Term.constr,glob_tactic_expr) generic_argument
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43807872..889e06a8 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -76,11 +76,12 @@ let rec prompt level =
   begin
     msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
-    let inst = read_line () in
+    let exit () = skip:=0;allskip:=0;raise Sys.Break in
+    let inst = try read_line () with End_of_file -> exit () in
     match inst with
     | ""  -> true
     | "s" -> false
-    | "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break
+    | "x" -> print_char (Char.chr 8); exit ()
     | "h"| "?" ->
       begin
         help ();