summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml36
-rw-r--r--proofs/clenvtac.mli6
-rw-r--r--proofs/logic.ml190
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli9
-rw-r--r--proofs/proof_type.ml3
-rw-r--r--proofs/proof_type.mli3
-rw-r--r--proofs/redexpr.ml21
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/refiner.mli3
-rw-r--r--proofs/tacexpr.ml26
-rw-r--r--proofs/tacmach.ml5
-rw-r--r--proofs/tacmach.mli3
-rw-r--r--proofs/tactic_debug.ml8
-rw-r--r--proofs/tactic_debug.mli4
16 files changed, 223 insertions, 111 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 92794ac3..f5204be5 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenvtac.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: clenvtac.ml 11709 2008-12-20 11:42:15Z msozeau $ *)
open Pp
open Util
@@ -47,16 +47,17 @@ let clenv_cast_meta clenv =
and crec_hd u =
match kind_of_term (strip_outer_cast u) with
- | Meta mv ->
- (try
+ | Meta mv ->
+ (try
let b = Typing.meta_type clenv.evd mv in
- if occur_meta b then u
- else mkCast (mkMeta mv, DEFAULTcast, b)
+ if occur_meta b then
+ raise (RefinerError (MetaInType b));
+ mkCast (mkMeta mv, DEFAULTcast, b)
with Not_found -> u)
- | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
- | Case(ci,p,c,br) ->
- mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
- | _ -> u
+ | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+ | Case(ci,p,c,br) ->
+ mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+ | _ -> u
in
crec
@@ -71,10 +72,15 @@ let clenv_pose_dependent_evars with_evars clenv =
clenv_pose_metas_as_evars clenv dep_mvs
-let clenv_refine with_evars clenv gls =
+let clenv_refine with_evars ?(with_classes=true) clenv gls =
let clenv = clenv_pose_dependent_evars with_evars clenv in
+ let evd' =
+ if with_classes then
+ Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd
+ else clenv.evd
+ in
tclTHEN
- (tclEVARS (evars_of clenv.evd))
+ (tclEVARS (evars_of evd'))
(refine (clenv_cast_meta clenv (clenv_value clenv)))
gls
@@ -105,11 +111,11 @@ let fail_quick_unif_flags = {
}
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms m n gls =
+let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
let env = pf_env gls in
let evd = create_goal_evar_defs (project gls) in
- let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in
+ let evd' = w_unify false env CONV ~flags m n evd in
tclIDTAC {it = gls.it; sigma = evars_of evd'}
-let unify m gls =
- let n = pf_concl gls in unifyTerms m n gls
+let unify ?(flags=fail_quick_unif_flags) m gls =
+ let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 29442ded..04a5eb57 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: clenvtac.mli 11166 2008-06-22 13:23:35Z herbelin $ i*)
+(*i $Id: clenvtac.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
(*i*)
open Util
@@ -21,8 +21,8 @@ open Unification
(*i*)
(* Tactics *)
-val unify : constr -> tactic
-val clenv_refine : evars_flag -> clausenv -> tactic
+val unify : ?flags:unify_flags -> constr -> tactic
+val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 21ee9a9f..a04216cb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
open Pp
open Util
@@ -37,6 +37,7 @@ type refiner_error =
| CannotApply of constr * constr
| NotWellTyped of constr
| NonLinearProof of constr
+ | MetaInType of constr
(* Errors raised by the tactics *)
| IntroNeedsProduct
@@ -57,29 +58,18 @@ let rec catchable_exception = function
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
|CannotFindWellTypedAbstraction _
|UnsolvableImplicit _)) -> true
+ | Typeclasses_errors.TypeClassError
+ (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
| _ -> false
+let error_no_such_hypothesis id =
+ error ("No such hypothesis: " ^ string_of_id id ^ ".")
+
(* Tells if the refiner should check that the submitted rules do not
produce invalid subgoals *)
let check = ref false
let with_check = Flags.with_option check
-(************************************************************************)
-(************************************************************************)
-(* Implementation of the structural rules (moving and deleting
- hypotheses around) *)
-
-(* The Clear tactic: it scans the context for hypotheses to be removed
- (instead of iterating on the list of identifier to be removed, which
- forces the user to give them in order). *)
-
-let clear_hyps sigma ids sign cl =
- let evdref = ref (Evd.create_goal_evar_defs sigma) in
- let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
- (hyps,concl,evars_of !evdref)
-
-(* The ClearBody tactic *)
-
(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
returns [tail::(f head (id,_,_) (rev tail))] *)
let apply_to_hyp sign id f =
@@ -97,6 +87,22 @@ let apply_to_hyp_and_dependent_on sign id f g =
let check_typability env sigma c =
if !check then let _ = type_of env sigma c in ()
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the structural rules (moving and deleting
+ hypotheses around) *)
+
+(* The Clear tactic: it scans the context for hypotheses to be removed
+ (instead of iterating on the list of identifier to be removed, which
+ forces the user to give them in order). *)
+
+let clear_hyps sigma ids sign cl =
+ let evdref = ref (Evd.create_goal_evar_defs sigma) in
+ let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+ (hyps,concl,evars_of !evdref)
+
+(* The ClearBody tactic *)
+
let recheck_typability (what,id) env sigma t =
try check_typability env sigma t
with _ ->
@@ -126,6 +132,82 @@ let remove_hyp_body env sigma id =
in
reset_with_named_context sign env
+(* Reordering of the context *)
+
+(* faire le minimum d'echanges pour que l'ordre donne soit un *)
+(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
+(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
+(* reculees par rapport aux autres (faire le contraire!) *)
+
+let mt_q = (Idmap.empty,[])
+let push_val y = function
+ (_,[] as q) -> q
+ | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
+let push_item x v (m,l) =
+ (Idmap.add x v m, (x,Idset.empty)::l)
+let mem_q x (m,_) = Idmap.mem x m
+let rec find_q x (m,q) =
+ let v = Idmap.find x m in
+ let m' = Idmap.remove x m in
+ let rec find accs acc = function
+ [] -> raise Not_found
+ | [(x',l)] ->
+ if x=x' then ((v,Idset.union accs l),(m',List.rev acc))
+ else raise Not_found
+ | (x',l as i)::((x'',l'')::q as itl) ->
+ if x=x' then
+ ((v,Idset.union accs l),
+ (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
+ else find (Idset.union l accs) (i::acc) itl in
+ find Idset.empty [] q
+
+let occur_vars_in_decl env hyps d =
+ if Idset.is_empty hyps then false else
+ let ohyps = global_vars_set_of_decl env d in
+ Idset.exists (fun h -> Idset.mem h ohyps) hyps
+
+let reorder_context env sign ord =
+ let ords = List.fold_right Idset.add ord Idset.empty in
+ if List.length ord <> Idset.cardinal ords then
+ error "Order list has duplicates";
+ let rec step ord expected ctxt_head moved_hyps ctxt_tail =
+ match ord with
+ | [] -> List.rev ctxt_tail @ ctxt_head
+ | top::ord' when mem_q top moved_hyps ->
+ let ((d,h),mh) = find_q top moved_hyps in
+ if occur_vars_in_decl env h d then
+ errorlabstrm "reorder_context"
+ (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+ str "before " ++
+ prlist_with_sep pr_spc pr_id
+ (Idset.elements (Idset.inter h
+ (global_vars_set_of_decl env d))));
+ step ord' expected ctxt_head mh (d::ctxt_tail)
+ | _ ->
+ (match ctxt_head with
+ | [] -> error_no_such_hypothesis (List.hd ord)
+ | (x,_,_ as d) :: ctxt ->
+ if Idset.mem x expected then
+ step ord (Idset.remove x expected)
+ ctxt (push_item x d moved_hyps) ctxt_tail
+ else
+ step ord expected
+ ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
+ step ord ords sign mt_q []
+
+let reorder_val_context env sign ord =
+ val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+
+
+
+
+let check_decl_position env sign (x,_,_ as d) =
+ let needed = global_vars_set_of_decl env d in
+ let deps = dependency_closure env (named_context_of_val sign) needed in
+ if List.mem x deps then
+ error ("Cannot create self-referring hypothesis "^string_of_id x);
+ x::deps
+
(* Auxiliary functions for primitive MOVE tactic
*
* [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
@@ -134,9 +216,6 @@ let remove_hyp_body env sigma id =
* on the right side [right] if [toleft=false].
* If [with_dep] then dependent hypotheses are moved accordingly. *)
-let error_no_such_hypothesis id =
- error ("No such hypothesis: " ^ string_of_id id ^ ".")
-
let rec get_hyp_after h = function
| [] -> error_no_such_hypothesis h
| (hyp,_,_) :: right ->
@@ -219,14 +298,23 @@ let rename_hyp id1 id2 sign =
(* Will only be used on terms given to the Refine rule which have meta
variables only in Application and Case *)
+let error_unsupported_deep_meta c =
+ errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+ strbrk "form contains metavariables deep inside the term is not " ++
+ strbrk "supported; try \"refine\" instead.")
+
let collect_meta_variables c =
- let rec collrec acc c = match kind_of_term c with
- | Meta mv -> mv::acc
- | Cast(c,_,_) -> collrec acc c
- | (App _| Case _) -> fold_constr collrec acc c
- | _ -> acc
- in
- List.rev(collrec [] c)
+ let rec collrec deep acc c = match kind_of_term c with
+ | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
+ | Cast(c,_,_) -> collrec deep acc c
+ | (App _| Case _) -> fold_constr (collrec deep) acc c
+ | _ -> fold_constr (collrec true) acc c
+ in
+ List.rev (collrec false [] c)
+
+let check_meta_variables c =
+ if not (list_distinct (collect_meta_variables c)) then
+ raise (RefinerError (NonLinearProof c))
let check_conv_leq_goal env sigma arg ty conclty =
if !check & not (is_conv_leq env sigma ty conclty) then
@@ -248,9 +336,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
*)
match kind_of_term trm with
| Meta _ ->
- if !check && occur_meta conclty then
- anomaly "refined called with a dependent meta";
- (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+ let conclty = nf_betaiota conclty in
+ if !check && occur_meta conclty then
+ raise (RefinerError (MetaInType conclty));
+ (mk_goal hyps conclty)::goalacc, conclty
| Cast (t,_, ty) ->
check_typability env sigma ty;
@@ -261,12 +350,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let (acc',hdty) =
match kind_of_term f with
| Ind _ | Const _
- when not (array_exists occur_meta l) (* we could be finer *)
- & (isInd f or has_polymorphic_type (destConst f))
- ->
+ when (isInd f or has_polymorphic_type (destConst f)) ->
(* Sort-polymorphism of definition and inductive types *)
goalacc,
- type_of_global_reference_knowing_parameters env sigma f l
+ type_of_global_reference_knowing_conclusion env sigma f conclty
| _ ->
mk_hdgoals sigma goal goalacc f
in
@@ -288,6 +375,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| _ ->
if occur_meta trm then
anomaly "refiner called with a meta in non app/case subterm";
+
let t'ty = goal_type_of env sigma trm in
check_conv_leq_goal env sigma trm t'ty conclty;
(goalacc,t'ty)
@@ -358,14 +446,19 @@ and mk_casegoals sigma goal goalacc p c =
let convert_hyp sign sigma (id,b,bt as d) =
- apply_to_hyp sign id
- (fun _ (_,c,ct) _ ->
- let env = Global.env_of_context sign in
- if !check && not (is_conv env sigma bt ct) then
- error ("Incorrect change of the type of "^(string_of_id id)^".");
- if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
- error ("Incorrect change of the body of "^(string_of_id id)^".");
- d)
+ let env = Global.env() in
+ let reorder = ref [] in
+ let sign' =
+ apply_to_hyp sign id
+ (fun _ (_,c,ct) _ ->
+ let env = Global.env_of_context sign in
+ if !check && not (is_conv env sigma bt ct) then
+ error ("Incorrect change of the type of "^(string_of_id id)^".");
+ if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
+ error ("Incorrect change of the body of "^(string_of_id id)^".");
+ if !check then reorder := check_decl_position env sign d;
+ d) in
+ reorder_val_context env sign' !reorder
(* Normalizing evars in a goal. Called by tactic Local_constraints
(i.e. when the sigma of the proof tree changes). Detect if the
@@ -418,7 +511,9 @@ let prim_refiner r sigma goal =
nexthyp,
cl,sigma
else
- (push_named_context_val (id,None,t) sign),cl,sigma in
+ (if !check && mem_named_context id (named_context_of_val sign) then
+ error "New variable is already declared";
+ push_named_context_val (id,None,t) sign,cl,sigma) in
let sg2 = mk_goal sign cl in
if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
@@ -478,8 +573,7 @@ let prim_refiner r sigma goal =
(mk_sign sign all, sigma)
| Refine c ->
- if not (list_distinct (collect_meta_variables c)) then
- raise (RefinerError (NonLinearProof c));
+ check_meta_variables c;
let (sgl,cl') = mk_refgoals sigma goal [] cl c in
let sgl = List.rev sgl in
(sgl, sigma)
@@ -518,6 +612,10 @@ let prim_refiner r sigma goal =
move_hyp withdep toleft (left,declfrom,right) hto in
([mk_goal hyps' cl], sigma)
+ | Order ord ->
+ let hyps' = reorder_val_context env sign ord in
+ ([mk_goal hyps' cl], sigma)
+
| Rename (id1,id2) ->
if !check & id1 <> id2 &&
List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
@@ -628,7 +726,7 @@ let prim_extractor subfun vl pft =
| Some (Prim (ThinBody _),[pf]) ->
subfun vl pf
- | Some (Prim (Move _),[pf]) ->
+ | Some (Prim (Move _|Order _),[pf]) ->
subfun vl pf
| Some (Prim (Rename (id1,id2)),[pf]) ->
diff --git a/proofs/logic.mli b/proofs/logic.mli
index def02c8c..2f3a0d89 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: logic.mli 10785 2008-04-13 21:41:54Z herbelin $ i*)
+(*i $Id: logic.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -54,6 +54,7 @@ type refiner_error =
| CannotApply of constr * constr
| NotWellTyped of constr
| NonLinearProof of constr
+ | MetaInType of constr
(*i Errors raised by the tactics i*)
| IntroNeedsProduct
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6d8f09ea..0aba9f5f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pfedit.ml 10850 2008-04-25 18:07:44Z herbelin $ *)
+(* $Id: pfedit.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
open Pp
open Util
@@ -34,6 +34,7 @@ open Safe_typing
type proof_topstate = {
mutable top_end_tac : tactic option;
top_init_tac : tactic option;
+ top_compute_guard : bool;
top_goal : goal;
top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
@@ -207,7 +208,7 @@ let set_xml_cook_proof f = xml_cook_proof := f
let cook_proof k =
let (pfs,ts) = get_state()
and ident = get_current_proof_name () in
- let {evar_concl=concl} = ts.top_goal
+ let {evar_concl=concl} = ts.top_goal
and strength = ts.top_strength in
let pfterm = extract_pftreestate pfs in
!xml_cook_proof (strength,pfs);
@@ -217,7 +218,7 @@ let cook_proof k =
const_entry_type = Some concl;
const_entry_opaque = true;
const_entry_boxed = false},
- strength, ts.top_hook))
+ ts.top_compute_guard, strength, ts.top_hook))
let current_proof_statement () =
let ts = get_topstate() in
@@ -251,11 +252,12 @@ let set_end_tac tac =
(* Modifying the current prooftree *)
(*********************************************************************)
-let start_proof na str sign concl ?init_tac hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
top_init_tac = init_tac;
+ top_compute_guard = compute_guard;
top_goal = top_goal;
top_strength = str;
top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 42c24081..464f6286 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pfedit.mli 10850 2008-04-25 18:07:44Z herbelin $ i*)
+(*i $Id: pfedit.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
(*i*)
open Util
@@ -80,7 +80,7 @@ val get_undo : unit -> int option
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
- ?init_tac:tactic -> declaration_hook -> unit
+ ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
@@ -104,10 +104,11 @@ val suspend_proof : unit -> unit
(*s [cook_proof opacity] turns the current proof (assumed completed) into
a constant with its name, kind and possible hook (see [start_proof]);
- it fails if there is no current proof of if it is not completed *)
+ it fails if there is no current proof of if it is not completed;
+ it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Refiner.pftreestate -> unit) ->
- identifier * (Entries.definition_entry * goal_kind * declaration_hook)
+ identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 41935c9c..1e673853 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_type.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(*i $Id: proof_type.ml 11639 2008-11-27 17:48:32Z barras $ *)
(*i*)
open Environ
@@ -37,6 +37,7 @@ type prim_rule =
| Thin of identifier list
| ThinBody of identifier list
| Move of bool * identifier * identifier move_location
+ | Order of identifier list
| Rename of identifier * identifier
| Change_evars
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index a7057a7d..21cd8b28 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_type.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: proof_type.mli 11639 2008-11-27 17:48:32Z barras $ i*)
(*i*)
open Environ
@@ -37,6 +37,7 @@ type prim_rule =
| Thin of identifier list
| ThinBody of identifier list
| Move of bool * identifier * identifier move_location
+ | Order of identifier list
| Rename of identifier * identifier
| Change_evars
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 072a38b6..ad8ee3a2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
open Pp
open Util
@@ -46,12 +46,13 @@ let set_strategy_one ref l =
Csymtable.set_transparent_const sp
| _ -> ()
-let cache_strategy str =
+let cache_strategy (_,str) =
List.iter
(fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
str
-let subst_strategy (_,subs,obj) =
+let subst_strategy (_,subs,(local,obj)) =
+ local,
list_smartmap
(fun (k,ql as entry) ->
let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
@@ -68,14 +69,16 @@ let map_strategy f l =
Some q' -> q' :: ql
| None -> ql) ql [] in
if ql'=[] then str else (lev,ql')::str) l [] in
- if l'=[] then None else Some l'
+ if l'=[] then None else Some (false,l')
-let export_strategy obj =
+let export_strategy (local,obj) =
+ if local then None else
map_strategy (function
EvalVarRef _ -> None
| EvalConstRef _ as q -> Some q) obj
-let classify_strategy (_,obj) = Substitute obj
+let classify_strategy (_,(local,_ as obj)) =
+ if local then Dispose else Substitute obj
let disch_ref ref =
match ref with
@@ -84,7 +87,8 @@ let disch_ref ref =
if c==c' then Some ref else Some (EvalConstRef c')
| _ -> Some ref
-let discharge_strategy (_,obj) =
+let discharge_strategy (_,(local,obj)) =
+ if local then None else
map_strategy disch_ref obj
let (inStrategy,outStrategy) =
@@ -98,8 +102,7 @@ let (inStrategy,outStrategy) =
let set_strategy local str =
- if local then cache_strategy str
- else Lib.add_anonymous_leaf (inStrategy str)
+ Lib.add_anonymous_leaf (inStrategy (local,str))
let _ =
Summary.declare_summary "Transparent constants and variables"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6e08e741..a9a1f51d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
open Pp
open Util
@@ -462,7 +462,7 @@ let weak_progress gls ptree =
(not (same_goal (List.hd gls.it) ptree.it))
let progress gls ptree =
- (not (ptree.sigma == gls.sigma)) ||
+ (not (eq_evar_map ptree.sigma gls.sigma)) ||
(weak_progress gls ptree)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 95130ac5..a6ba3af5 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: refiner.mli 10879 2008-05-01 22:14:20Z msozeau $ i*)
+(*i $Id: refiner.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
(*i*)
open Term
@@ -137,6 +137,7 @@ exception FailError of int * Pp.std_ppcmds
level or do nothing. *)
val catch_failerror : exn -> unit
+val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclREPEAT : tactic -> tactic
val tclREPEAT_MAIN : tactic -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8e51171f..66136afa 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: tacexpr.ml 11739 2009-01-02 19:33:19Z herbelin $ i*)
open Names
open Topconstr
@@ -58,12 +58,7 @@ let make_red_flag =
add_flag
{rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
-type hyp_location_flag = (* To distinguish body and type of local defs *)
- | InHyp
- | InHypTypeOnly
- | InHypValueOnly
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
type 'id move_location =
| MoveAfter of 'id
@@ -103,7 +98,6 @@ 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*
@@ -133,16 +127,15 @@ type multi =
| RepeatStar
| RepeatPlus
-type pattern_expr = constr_expr
-
(* Type of patterns *)
type 'a match_pattern =
| Term of 'a
- | Subterm of identifier option * 'a
+ | Subterm of bool * identifier option * 'a
(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
| Hyp of name located * 'a match_pattern
+ | Def of name located * 'a match_pattern * 'a match_pattern
(* Type of a Match rule for Match Context and Match *)
type ('a,'t) match_rule =
@@ -158,7 +151,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacExact of 'constr
| TacExactNoCheck of 'constr
| TacVmCastNoCheck of 'constr
- | TacApply of advanced_flag * evars_flag * 'constr with_bindings list
+ | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
+ ('id * intro_pattern_expr located option) option
| TacElim of evars_flag * 'constr with_bindings *
'constr with_bindings option
| TacElimType of 'constr
@@ -170,7 +164,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacCofix of identifier option
| TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
| TacCut of 'constr
- | TacAssert of 'tac option * intro_pattern_expr located * 'constr
+ | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
| TacGeneralize of ('constr with_occurrences * name) list
| TacGeneralizeDep of 'constr
| TacLetTac of name * 'constr * 'id gclause * letin_flag
@@ -287,7 +281,7 @@ and glob_tactic_expr =
type raw_tactic_expr =
(constr_expr,
- pattern_expr,
+ constr_pattern_expr,
reference or_by_notation,
reference or_by_notation,
reference,
@@ -296,7 +290,7 @@ type raw_tactic_expr =
type raw_atomic_tactic_expr =
(constr_expr, (* constr *)
- pattern_expr, (* pattern *)
+ constr_pattern_expr, (* pattern *)
reference or_by_notation, (* evaluable reference *)
reference or_by_notation, (* inductive *)
reference, (* ltac reference *)
@@ -305,7 +299,7 @@ type raw_atomic_tactic_expr =
type raw_tactic_arg =
(constr_expr,
- pattern_expr,
+ constr_pattern_expr,
reference or_by_notation,
reference or_by_notation,
reference,
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6bbaff08..bf194d47 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
open Pp
open Util
@@ -202,6 +202,9 @@ let thin_body_no_check ids gl =
let move_hyp_no_check with_dep id1 id2 gl =
refiner (Prim (Move (with_dep,id1,id2))) gl
+let order_hyps idl gl =
+ refiner (Prim (Order idl)) gl
+
let rec rename_hyp_no_check l gl = match l with
| [] -> tclIDTAC gl
| (id1,id2)::l ->
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 2fc66e71..cdcb8bfd 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacmach.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
(*i*)
open Names
@@ -133,6 +133,7 @@ val thin_body_no_check : identifier list -> tactic
val move_hyp_no_check :
bool -> identifier -> identifier move_location -> tactic
val rename_hyp_no_check : (identifier*identifier) list -> tactic
+val order_hyps : identifier list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 2e19011f..7aa57d9b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tactic_debug.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: tactic_debug.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
open Names
open Constrextern
@@ -129,7 +129,7 @@ let hyp_bound = function
| Name id -> " (bound to "^(Names.string_of_id id)^")"
(* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,c) ido =
+let db_matched_hyp debug env (id,_,c) ido =
if debug <> DebugOff & !skip = 0 then
msgnl (str "Hypothesis " ++
str ((Names.string_of_id id)^(hyp_bound ido)^
@@ -148,8 +148,8 @@ let db_mc_pattern_success debug =
let pp_match_pattern env = function
| Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
- | Subterm (o,c) ->
- Subterm (o,(extern_constr_pattern (names_of_rel_context env) c))
+ | Subterm (b,o,c) ->
+ Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c))
(* Prints a failure message for an hypothesis pattern *)
let db_hyp_pattern_failure debug env (na,hyp) =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 6de8244d..63c89547 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tactic_debug.mli 9092 2006-08-28 11:42:14Z bertot $ i*)
+(*i $Id: tactic_debug.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
open Environ
open Pattern
@@ -45,7 +45,7 @@ val db_pattern_rule :
(* Prints a matched hypothesis *)
val db_matched_hyp :
- debug_info -> env -> identifier * constr -> name -> unit
+ debug_info -> env -> identifier * constr option * constr -> name -> unit
(* Prints the matched conclusion *)
val db_matched_concl : debug_info -> env -> constr -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-13 13:36:50 +0000