From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- proofs/evar_refiner.ml | 4 ++-- proofs/logic.ml | 6 +++--- proofs/redexpr.ml | 17 ++++++++++++----- proofs/redexpr.mli | 4 +++- proofs/refiner.ml | 4 ++-- proofs/tacexpr.ml | 15 ++++++++------- proofs/tactic_debug.ml | 5 +++-- 7 files changed, 33 insertions(+), 22 deletions(-) (limited to 'proofs') 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 (); -- cgit v1.2.3