summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/decl_expr.mli108
-rw-r--r--proofs/decl_mode.ml121
-rw-r--r--proofs/decl_mode.mli73
-rw-r--r--proofs/evar_refiner.ml6
-rw-r--r--proofs/evar_refiner.mli4
-rw-r--r--proofs/logic.ml63
-rw-r--r--proofs/pfedit.ml24
-rw-r--r--proofs/pfedit.mli6
-rw-r--r--proofs/proof_trees.ml27
-rw-r--r--proofs/proof_trees.mli6
-rw-r--r--proofs/proof_type.ml17
-rw-r--r--proofs/proof_type.mli16
-rw-r--r--proofs/redexpr.ml4
-rw-r--r--proofs/refiner.ml226
-rw-r--r--proofs/refiner.mli32
-rw-r--r--proofs/tacexpr.ml4
-rw-r--r--proofs/tactic_debug.ml2
-rw-r--r--proofs/tactic_debug.mli8
18 files changed, 582 insertions, 165 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
new file mode 100644
index 00000000..24af3842
--- /dev/null
+++ b/proofs/decl_expr.mli
@@ -0,0 +1,108 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Util
+open Tacexpr
+
+type ('constr,'tac) justification =
+ By_tactic of 'tac
+| Automated of 'constr list
+
+type 'it statement =
+ {st_label:name;
+ st_it:'it}
+
+type thesis_kind =
+ Plain
+ | Sub of int
+ | For of identifier
+
+type 'this or_thesis =
+ This of 'this
+ | Thesis of thesis_kind
+
+type side = Lhs | Rhs
+
+type elim_type =
+ ET_Case_analysis
+ | ET_Induction
+
+type block_type =
+ B_proof
+ | B_claim
+ | B_focus
+ | B_elim of elim_type
+
+type ('it,'constr,'tac) cut =
+ {cut_stat: 'it statement;
+ cut_by: ('constr,'tac) justification}
+
+type ('var,'constr) hyp =
+ Hvar of 'var
+ | Hprop of 'constr statement
+
+type ('constr,'tac) casee =
+ Real of 'constr
+ | Virtual of ('constr,'constr,'tac) cut
+
+type ('hyp,'constr,'pat,'tac) bare_proof_instr =
+ | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+ | Pcut of ('constr or_thesis,'constr,'tac) cut
+ | Prew of side * ('constr,'constr,'tac) cut
+ | Passume of ('hyp,'constr) hyp list
+ | Plet of ('hyp,'constr) hyp list
+ | Pgiven of ('hyp,'constr) hyp list
+ | Pconsider of 'constr*('hyp,'constr) hyp list
+ | Pclaim of 'constr statement
+ | Pfocus of 'constr statement
+ | Pdefine of identifier * 'hyp list * 'constr
+ | Pcast of identifier or_thesis * 'constr
+ | Psuppose of ('hyp,'constr) hyp list
+ | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+ | Ptake of 'constr list
+ | Pper of elim_type * ('constr,'tac) casee
+ | Pend of block_type
+ | Pescape
+
+type emphasis = int
+
+type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+ {emph: emphasis;
+ instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+
+
+type raw_proof_instr =
+ ((identifier*(Topconstr.constr_expr option)) located,
+ Topconstr.constr_expr,
+ Topconstr.cases_pattern_expr,
+ raw_tactic_expr) gen_proof_instr
+
+type glob_proof_instr =
+ ((identifier*(Genarg.rawconstr_and_expr option)) located,
+ Genarg.rawconstr_and_expr,
+ Topconstr.cases_pattern_expr,
+ Tacexpr.glob_tactic_expr) gen_proof_instr
+
+type proof_pattern =
+ {pat_vars: Term.types statement list;
+ pat_aliases: (Term.constr*Term.types) statement list;
+ pat_constr: Term.constr;
+ pat_typ: Term.types;
+ pat_pat: Rawterm.cases_pattern;
+ pat_expr: Topconstr.cases_pattern_expr}
+
+type proof_instr =
+ (Term.constr statement,
+ Term.constr,
+ proof_pattern,
+ Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
new file mode 100644
index 00000000..094c5625
--- /dev/null
+++ b/proofs/decl_mode.ml
@@ -0,0 +1,121 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Util
+
+let daimon_flag = ref false
+
+let set_daimon_flag () = daimon_flag:=true
+let clear_daimon_flag () = daimon_flag:=false
+let get_daimon_flag () = !daimon_flag
+
+type command_mode =
+ Mode_tactic
+ | Mode_proof
+ | Mode_none
+
+let mode_of_pftreestate pts =
+ let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
+ if goal.evar_extra = None then
+ Mode_tactic
+ else
+ Mode_proof
+
+let get_current_mode () =
+ try
+ mode_of_pftreestate (Pfedit.get_pftreestate ())
+ with _ -> Mode_none
+
+let check_not_proof_mode str =
+ if get_current_mode () = Mode_proof then
+ error str
+
+type split_tree=
+ Push of (Idset.t * split_tree)
+ | Split of (Idset.t * inductive * (Idset.t * split_tree) option array)
+ | Pop of split_tree
+ | End_of_branch of (identifier * int)
+
+type elim_kind =
+ EK_dep of split_tree
+ | EK_nodep
+ | EK_unknown
+
+type per_info =
+ {per_casee:constr;
+ per_ctype:types;
+ per_ind:inductive;
+ per_pred:constr;
+ per_args:constr list;
+ per_params:constr list;
+ per_nparams:int}
+
+type stack_info =
+ Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
+ | Suppose_case
+ | Claim
+ | Focus_claim
+
+type pm_info =
+ { pm_last: Names.name (* anonymous if none *);
+ pm_hyps: Idset.t;
+ pm_partial_goal : constr ; (* partial goal construction *)
+ pm_subgoals : (metavariable*constr) list;
+ pm_stack : stack_info list }
+
+let pm_in,pm_out = Dyn.create "pm_info"
+
+let get_info gl=
+ match gl.evar_extra with
+ None -> invalid_arg "get_info"
+ | Some extra ->
+ try pm_out extra with _ -> invalid_arg "get_info"
+
+let get_stack pts =
+ let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
+ info.pm_stack
+
+let get_top_stack pts =
+ let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
+ info.pm_stack
+
+let get_end_command pts =
+ match mode_of_pftreestate pts with
+ Mode_proof ->
+ Some
+ begin
+ match get_top_stack pts with
+ [] -> "\"end proof\""
+ | Claim::_ -> "\"end claim\""
+ | Focus_claim::_-> "\"end focus\""
+ | (Suppose_case :: Per (et,_,_,_) :: _
+ | Per (et,_,_,_) :: _ ) ->
+ begin
+ match et with
+ Decl_expr.ET_Case_analysis ->
+ "\"end cases\" or start a new case"
+ | Decl_expr.ET_Induction ->
+ "\"end induction\" or start a new case"
+ end
+ | _ -> anomaly "lonely suppose"
+ end
+ | Mode_tactic ->
+ begin
+ try
+ ignore
+ (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
+ Some "\"return\""
+ with Not_found -> None
+ end
+ | Mode_none ->
+ error "no proof in progress"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
new file mode 100644
index 00000000..0dd1cb33
--- /dev/null
+++ b/proofs/decl_mode.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Evd
+open Tacmach
+
+val set_daimon_flag : unit -> unit
+val clear_daimon_flag : unit -> unit
+val get_daimon_flag : unit -> bool
+
+type command_mode =
+ Mode_tactic
+ | Mode_proof
+ | Mode_none
+
+val mode_of_pftreestate : pftreestate -> command_mode
+
+val get_current_mode : unit -> command_mode
+
+val check_not_proof_mode : string -> unit
+
+type split_tree=
+ Push of (Idset.t * split_tree)
+ | Split of (Idset.t * inductive * (Idset.t*split_tree) option array)
+ | Pop of split_tree
+ | End_of_branch of (identifier * int)
+
+type elim_kind =
+ EK_dep of split_tree
+ | EK_nodep
+ | EK_unknown
+
+
+type per_info =
+ {per_casee:constr;
+ per_ctype:types;
+ per_ind:inductive;
+ per_pred:constr;
+ per_args:constr list;
+ per_params:constr list;
+ per_nparams:int}
+
+type stack_info =
+ Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
+ | Suppose_case
+ | Claim
+ | Focus_claim
+
+type pm_info =
+ { pm_last: Names.name (* anonymous if none *);
+ pm_hyps: Idset.t;
+ pm_partial_goal : constr ; (* partial goal construction *)
+ pm_subgoals : (metavariable*constr) list;
+ pm_stack : stack_info list }
+
+val pm_in : pm_info -> Dyn.t
+
+val get_info : Proof_type.goal -> pm_info
+
+val get_end_command : pftreestate -> string option
+
+val get_stack : pftreestate -> stack_info list
+
+val get_top_stack : pftreestate -> stack_info list
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 7a23d052..79f01ba1 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 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evar_refiner.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
open Util
open Names
@@ -22,7 +22,7 @@ open Refiner
(* w_tactic pour instantiate *)
-let w_refine env ev rawc evd =
+let w_refine ev rawc evd =
if Evd.is_defined (evars_of evd) ev then
error "Instantiate called on already-defined evar";
let e_info = Evd.find (evars_of evd) ev in
@@ -45,5 +45,5 @@ let instantiate_pf_com n com pfts =
let env = Evd.evar_env evi in
let rawc = Constrintern.intern_constr sigma env com in
let evd = create_evar_defs sigma in
- let evd' = w_refine env sp rawc evd in
+ let evd' = w_refine sp rawc evd in
change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 9880f2f0..baa6b19a 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
(*i*)
open Names
@@ -18,7 +18,7 @@ open Refiner
(* Refinement of existential variables. *)
-val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
+val w_refine : evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
val instantiate_pf_com :
int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ffbc0d56..e40d1232 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
open Pp
open Util
@@ -80,15 +80,15 @@ let clear_hyps ids gl =
error (string_of_id id'^
" is used in hypothesis "^string_of_id id))
(global_vars_set_of_decl env d) in
- clear_hyps ids fcheck gl.evar_hyps in
+ clear_hyps ids fcheck gl.evar_hyps in
let ncl = gl.evar_concl in
- if !check && cleared_ids<>[] then
- Idset.iter
- (fun id' ->
- if List.mem id' cleared_ids then
- error (string_of_id id'^" is used in conclusion"))
- (global_vars_set env ncl);
- mk_goal nhyps ncl
+ if !check && cleared_ids<>[] then
+ Idset.iter
+ (fun id' ->
+ if List.mem id' cleared_ids then
+ error (string_of_id id'^" is used in conclusion"))
+ (global_vars_set_drop_evar env ncl);
+ mk_goal nhyps ncl gl.evar_extra
(* The ClearBody tactic *)
@@ -155,7 +155,7 @@ let split_sign hfrom hto l =
else
splitrec (d::left) (toleft or (hyp = hto)) right
in
- splitrec [] false l
+ splitrec [] false l
let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
let env = Global.env() in
@@ -214,19 +214,25 @@ let check_forward_dependencies id tail =
^ (string_of_id id')))
tail
+let check_goal_dependency id cl =
+ let env = Global.env() in
+ if Idset.mem id (global_vars_set_drop_evar env cl) then
+ error (string_of_id id^" is used in conclusion")
let rename_hyp id1 id2 sign =
apply_to_hyp_and_dependent_on sign id1
(fun (_,b,t) _ -> (id2,b,t))
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
-let replace_hyp sign id d =
+let replace_hyp sign id d cl =
+ if !check then
+ check_goal_dependency id cl;
apply_to_hyp sign id
(fun sign _ tail ->
- if !check then
- (check_backward_dependencies sign d;
- check_forward_dependencies id tail);
- d)
+ if !check then
+ (check_backward_dependencies sign d;
+ check_forward_dependencies id tail);
+ d)
(* why we dont check that id does not appear in tail ??? *)
let insert_after_hyp sign id d =
@@ -264,6 +270,7 @@ let goal_type_of env sigma c =
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
(*
if not (occur_meta trm) then
let t'ty = (unsafe_machine env sigma trm).uj_type in
@@ -284,9 +291,14 @@ 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_inductive_knowing_parameters env sigma (destInd f) l)
- else mk_hdgoals sigma goal goalacc f
+ match kind_of_term f with
+ | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
+ when not (array_exists occur_meta l) (* we could be finer *) ->
+ (* Sort-polymorphism of definition and inductive types *)
+ goalacc,
+ type_of_global_reference_knowing_parameters env sigma f l
+ | _ ->
+ mk_hdgoals sigma goal goalacc f
in
let (acc'',conclty') =
mk_arggoals sigma goal acc' hdty (Array.to_list l) in
@@ -315,6 +327,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
and mk_hdgoals sigma goal goalacc trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
@@ -326,8 +339,10 @@ 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_inductive_knowing_parameters env sigma (destInd f) l)
+ if isInd f or isConst f
+ & not (array_exists occur_meta l) (* we could be finer *)
+ then
+ (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
else mk_hdgoals sigma goal goalacc f
in
mk_arggoals sigma goal acc' hdty (Array.to_list l)
@@ -392,6 +407,7 @@ let prim_refiner r sigma goal =
let env = evar_env goal in
let sign = goal.evar_hyps in
let cl = goal.evar_concl in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match r with
(* Logical rules *)
| Intro id ->
@@ -416,12 +432,12 @@ let prim_refiner r sigma goal =
(match kind_of_term (strip_outer_cast cl) with
| Prod (_,c1,b) ->
if occur_meta c1 then error_use_instantiate();
- let sign' = replace_hyp sign id (id,None,c1) in
+ let sign' = replace_hyp sign id (id,None,c1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
[sg]
| LetIn (_,c1,t1,b) ->
if occur_meta c1 then error_use_instantiate();
- let sign' = replace_hyp sign id (id,Some c1,t1) in
+ let sign' = replace_hyp sign id (id,Some c1,t1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
[sg]
| _ ->
@@ -474,7 +490,8 @@ let prim_refiner r sigma goal =
let _ = find_coinductive env sigma b in ()
with Not_found ->
error ("All methods must construct elements " ^
- "in coinductive types")
+ "in coinductiv-> goal
+e types")
in
let all = (f,cl)::others in
List.iter (fun (_,c) -> check_is_coind env c) all;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fa6f8c37..565c9547 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
open Pp
open Util
@@ -150,6 +150,14 @@ let subtree_solved () =
is_complete_proof (proof_of_pftreestate pts) &
not (is_top_pftreestate pts)
+let tree_solved () =
+ let pts = get_pftreestate () in
+ is_complete_proof (proof_of_pftreestate pts)
+
+let top_tree_solved () =
+ let pts = get_pftreestate () in
+ is_complete_proof (proof_of_pftreestate (top_of_tree pts))
+
(*********************************************************************)
(* Undo functions *)
(*********************************************************************)
@@ -243,7 +251,7 @@ let set_end_tac tac =
(*********************************************************************)
let start_proof na str sign concl hook =
- let top_goal = mk_goal sign concl in
+ let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
top_goal = top_goal;
@@ -253,7 +261,6 @@ let start_proof na str sign concl hook =
start(na,ts);
set_current_proof na
-
let solve_nth k tac =
let pft = get_pftreestate () in
if not (List.mem (-1) (cursor_of_pftreestate pft)) then
@@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven
let traverse_next_unproven () = mutate next_unproven
-
(* The goal focused on *)
let focus_n = ref 0
let make_focus n = focus_n := n
@@ -317,5 +323,11 @@ let focus () = !focus_n
let focused_goal () = let n = !focus_n in if n=0 then 1 else n
let reset_top_of_tree () =
- let pts = get_pftreestate () in
- if not (is_top_pftreestate pts) then mutate top_of_tree
+ mutate top_of_tree
+
+let reset_top_of_script () =
+ mutate (fun pts ->
+ try
+ up_until_matching_rule is_proof_instr pts
+ with Not_found -> top_of_tree pts)
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ca379d2e..8c0c7f55 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 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
(*i*)
open Util
@@ -172,8 +172,12 @@ val make_focus : int -> unit
val focus : unit -> int
val focused_goal : unit -> int
val subtree_solved : unit -> bool
+val tree_solved : unit -> bool
+val top_tree_solved : unit -> bool
val reset_top_of_tree : unit -> unit
+val reset_top_of_script : unit -> unit
+
val traverse : int -> unit
val traverse_nth_goal : int -> unit
val traverse_next_unproven : unit -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 7e299b89..9d70d012 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: proof_trees.ml 6113 2004-09-17 20:28:19Z barras $ *)
+(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
open Closure
open Util
@@ -18,6 +18,7 @@ open Sign
open Evd
open Environ
open Evarutil
+open Decl_expr
open Proof_type
open Tacred
open Typing
@@ -32,9 +33,9 @@ let is_bind = function
(* Functions on goals *)
-let mk_goal hyps cl =
+let mk_goal hyps cl extra =
{ evar_hyps = hyps; evar_concl = cl;
- evar_body = Evar_empty}
+ evar_body = Evar_empty; evar_extra = extra }
(* Functions on proof trees *)
@@ -52,7 +53,7 @@ let children_of_proof pf =
let goal_of_proof pf = pf.goal
let subproof_of_proof pf = match pf.ref with
- | Some (Tactic (_,pf), _) -> pf
+ | Some (Nested (_,pf), _) -> pf
| _ -> failwith "subproof_of_proof"
let status_of_proof pf = pf.open_subgoals
@@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0
let is_leaf_proof pf = (pf.ref = None)
let is_tactic_proof pf = match pf.ref with
- | Some (Tactic _, _) -> true
+ | Some (Nested (Tactic _,_),_) -> true
| _ -> false
@@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed env ccl s =
let pf_lookup_index_as_renamed env ccl n =
Detyping.lookup_index_as_renamed env ccl n
+(* Functions on rules (Proof mode) *)
+
+let is_dem_rule = function
+ Decl_proof _ -> true
+ | _ -> false
+
+let is_proof_instr = function
+ Nested(Proof_instr (_,_),_) -> true
+ | _ -> false
+
+let is_focussing_command = function
+ Decl_proof b -> b
+ | Nested (Proof_instr (b,_),_) -> b
+ | _ -> false
+
+
(*********************************************************************)
(* Pretty printing functions *)
(*********************************************************************)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index cbf91c8a..f9b64f41 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_trees.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: proof_trees.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
(*i*)
open Util
@@ -21,7 +21,7 @@ open Proof_type
(* This module declares readable constraints, and a few utilities on
constraints and proof trees *)
-val mk_goal : named_context_val -> constr -> goal
+val mk_goal : named_context_val -> constr -> Dyn.t option -> goal
val rule_of_proof : proof_tree -> rule
val ref_of_proof : proof_tree -> (rule * proof_tree list)
@@ -36,6 +36,8 @@ val is_tactic_proof : proof_tree -> bool
val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option
val pf_lookup_index_as_renamed : env -> constr -> int -> int option
+val is_proof_instr : rule -> bool
+val is_focussing_command : rule -> bool
(*s Pretty printing functions. *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 009e9d5b..abe31624 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 7639 2005-12-02 10:01:15Z gregoire $ *)
+(*i $Id: proof_type.ml 9244 2006-10-16 17:11:44Z barras $ *)
(*i*)
open Environ
@@ -16,6 +16,7 @@ open Libnames
open Term
open Util
open Tacexpr
+open Decl_expr
open Rawterm
open Genarg
open Nametab
@@ -39,12 +40,6 @@ type prim_rule =
| Move of bool * identifier * identifier
| Rename of identifier * identifier
-(*s Proof trees.
- [ref] = [None] if the goal has still to be proved,
- and [Some (r,l)] if the rule [r] was applied to the goal
- and gave [l] as subproofs to be completed.
- if [ref = (Some(Tactic (t,p),l))] then [p] is the proof
- that the goal can be proven if the goals in [l] are solved. *)
type proof_tree = {
open_subgoals : int;
goal : goal;
@@ -52,9 +47,15 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Tactic of tactic_expr * proof_tree
+ | Nested of compound_rule * proof_tree
+ | Decl_proof of bool
+ | Daimon
| Change_evars
+and compound_rule=
+ | Tactic of tactic_expr * bool
+ | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
+
and goal = evar_info
and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 0e42dcba..d87c1298 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 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: proof_type.mli 9244 2006-10-16 17:11:44Z barras $ i*)
(*i*)
open Environ
@@ -16,6 +16,7 @@ open Libnames
open Term
open Util
open Tacexpr
+open Decl_expr
open Rawterm
open Genarg
open Nametab
@@ -46,7 +47,7 @@ type prim_rule =
evar_body = Evar_Empty;
evar_info = { pgm : [The Realizer pgm if any]
lc : [Set of evar num occurring in subgoal] }}
- sigma = { stamp = [an int characterizing the ed field, for quick compare]
+ sigma = { stamp = [an int chardacterizing the ed field, for quick compare]
ed : [A set of existential variables depending in the subgoal]
number of first evar,
it = { evar_concl = [the type of first evar]
@@ -71,7 +72,7 @@ type prim_rule =
[ref] = [None] if the goal has still to be proved,
and [Some (r,l)] if the rule [r] was applied to the goal
and gave [l] as subproofs to be completed.
- if [ref = (Some(Tactic (t,p),l))] then [p] is the proof
+ if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
that the goal can be proven if the goals in [l] are solved. *)
type proof_tree = {
open_subgoals : int;
@@ -80,9 +81,16 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Tactic of tactic_expr * proof_tree
+ | Nested of compound_rule * proof_tree
+ | Decl_proof of bool
+ | Daimon
| Change_evars
+and compound_rule=
+ (* the boolean of Tactic tells if the default tactic is used *)
+ | Tactic of tactic_expr * bool
+ | Proof_instr of bool * proof_instr
+
and goal = evar_info
and tactic = goal sigma -> (goal list sigma * validation)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index eb47fc2e..ad277caa 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: redexpr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *)
open Pp
open Util
@@ -24,7 +24,7 @@ open RedFlags
(* call by value normalisation function using the virtual machine *)
let cbv_vm env _ c =
let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
- Vconv.cbv_vm env c ctyp
+ Vnorm.cbv_vm env c ctyp
let set_opaque_const sp =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 067ae471..70a0e3db 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: refiner.ml 9261 2006-10-23 10:01:40Z barras $ *)
open Pp
open Util
@@ -43,6 +43,31 @@ let and_status = List.fold_left (+) 0
let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
+
+let descend n p =
+ match p.ref with
+ | None -> error "It is a leaf."
+ | Some(r,pfl) ->
+ if List.length pfl >= n then
+ (match list_chop (n-1) pfl with
+ | left,(wanted::right) ->
+ (wanted,
+ (fun pfl' ->
+ if (List.length pfl' = 1)
+ & (List.hd pfl').goal = wanted.goal
+ then
+ let pf' = List.hd pfl' in
+ let spfl = left@(pf'::right) in
+ let newstatus = and_status (List.map pf_status spfl) in
+ { p with
+ open_subgoals = newstatus;
+ ref = Some(r,spfl) }
+ else
+ error "descend: validation"))
+ | _ -> assert false)
+ else
+ error "Too few subproofs"
+
(* Normalizing evars in a goal. Called by tactic Local_constraints
(i.e. when the sigma of the proof tree changes). Detect if the
goal is unchanged *)
@@ -50,10 +75,10 @@ let norm_goal sigma gl =
let red_fun = Evarutil.nf_evar sigma in
let ncl = red_fun gl.evar_concl in
let ngl =
- { evar_concl = ncl;
- evar_hyps = map_named_val red_fun gl.evar_hyps;
- evar_body = gl.evar_body} in
- if Evd.eq_evar_info ngl gl then None else Some ngl
+ { gl with
+ evar_concl = ncl;
+ evar_hyps = map_named_val red_fun gl.evar_hyps } in
+ if Evd.eq_evar_info ngl gl then None else Some ngl
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -91,9 +116,9 @@ let rec frontier p =
(List.flatten gll,
(fun retpfl ->
let pfl' = mapshape (List.map List.length gll) vl retpfl in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}))
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}))
let rec frontier_map_rec f n p =
@@ -111,9 +136,9 @@ let rec frontier_map_rec f n p =
(fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
(n,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_map f n p =
let nmax = p.open_subgoals in
@@ -137,9 +162,9 @@ let rec frontier_mapi_rec f i p =
(fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
(i,[]) pfl in
let pfl' = List.rev rpfl' in
- { open_subgoals = and_status (List.map pf_status pfl');
- goal = p.goal;
- ref = Some(r,pfl')}
+ { p with
+ open_subgoals = and_status (List.map pf_status pfl');
+ ref = Some(r,pfl')}
let frontier_mapi f p = frontier_mapi_rec f 1 p
@@ -152,50 +177,35 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
(* leaf g is the canonical incomplete proof of a goal g *)
-let leaf g = {
- open_subgoals = 1;
- goal = g;
- ref = None }
-
-(* Tactics table. *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
- if Hashtbl.mem tac_tab s then
- errorlabstrm ("Refiner.add_tactic: ")
- (str ("Cannot redeclare tactic "^s));
- Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
- if Hashtbl.mem tac_tab s then begin
- Hashtbl.remove tac_tab s;
- warning ("Overwriting definition of tactic "^s)
- end;
- Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
- try
- Hashtbl.find tac_tab s
- with Not_found ->
- errorlabstrm "Refiner.lookup_tactic"
- (str"The tactic " ++ str s ++ str" is not installed")
-
+let leaf g =
+ { open_subgoals = 1;
+ goal = g;
+ ref = None }
(* refiner r is a tactic applying the rule r *)
let check_subproof_connection gl spfl =
list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
-let abstract_tactic_expr te tacfun gls =
- let (sgl_sigma,v) = tacfun gls in
- let hidden_proof = v (List.map leaf sgl_sigma.it) in
+
+let abstract_operation syntax semantics gls =
+ let (sgl_sigma,validation) = semantics gls in
+ let hidden_proof = validation (List.map leaf sgl_sigma.it) in
(sgl_sigma,
fun spfl ->
assert (check_subproof_connection sgl_sigma.it spfl);
{ open_subgoals = and_status (List.map pf_status spfl);
goal = gls.it;
- ref = Some(Tactic(te,hidden_proof),spfl) })
+ ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_tactic_expr ?(dflt=false) te tacfun gls =
+ abstract_operation (Tactic(te,dflt)) tacfun gls
+
+let abstract_tactic ?(dflt=false) te =
+ abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
+
+let abstract_extended_tactic ?(dflt=false) s args =
+ abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
let refiner = function
| Prim pr as r ->
@@ -209,8 +219,21 @@ let refiner = function
goal = goal_sigma.it;
ref = Some(r,spfl) })))
- | Tactic _ -> failwith "Refiner: should not occur"
+
+ | Nested (_,_) | Decl_proof _ ->
+ failwith "Refiner: should not occur"
+ (* Daimon is a canonical unfinished proof *)
+
+ | Daimon ->
+ fun gls ->
+ ({it=[];sigma=gls.sigma},
+ fun spfl ->
+ assert (spfl=[]);
+ { open_subgoals = 0;
+ goal = gls.it;
+ ref = Some(Daimon,[])})
+
(* [Local_constraints lc] makes the local constraints be [lc] and
normalizes evars *)
@@ -237,19 +260,11 @@ let local_Constraints gl = refiner Change_evars gl
let norm_evar_tac = local_Constraints
-(*
-let vernac_tactic (s,args) =
- let tacfun = lookup_tactic s args in
- abstract_extra_tactic s args tacfun
-*)
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
-
-let abstract_extended_tactic s args =
- abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
-
-let vernac_tactic (s,args) =
- let tacfun = lookup_tactic s args in
- abstract_extended_tactic s args tacfun
+let norm_evar_proof sigma pf =
+ let nf_subgoal i sgl =
+ let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
+ v (List.map leaf gll.it) in
+ frontier_mapi nf_subgoal pf
(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
@@ -271,14 +286,16 @@ let extract_open_proof sigma pf =
let rec proof_extractor vl = function
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
- | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+ | {ref=Some(Nested(_,hidden_proof),spfl)} ->
let sgl,v = frontier hidden_proof in
let flat_proof = v spfl in
proof_extractor vl flat_proof
-
+
| {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
+
+ | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
- | {ref=None;goal=goal} ->
+ | {ref=(None|Some(Daimon,[]));goal=goal} ->
let visible_rels =
map_succeed
(fun id ->
@@ -555,6 +572,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS
let tclIFTHENSVELSE=ite_gen tclTHENSV
+let tclIFTHENTRYELSEMUST tac1 tac2 gl =
+ tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
(* Fails if a tactic did not solve the goal *)
let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
@@ -633,7 +652,6 @@ let tactic_list_tactic tac gls =
-
(* The type of proof-trees state and a few utilities
A proof-tree state is built from a proof-tree, a set of global
constraints, and a stack which allows to navigate inside the
@@ -665,41 +683,19 @@ let nth_goal_of_pftreestate n pts =
try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
with Invalid_argument _ | Failure _ -> non_existent_goal n
-let descend n p =
- match p.ref with
- | None -> error "It is a leaf."
- | Some(r,pfl) ->
- if List.length pfl >= n then
- (match list_chop (n-1) pfl with
- | left,(wanted::right) ->
- (wanted,
- (fun pfl' ->
- if (List.length pfl' = 1)
- & (List.hd pfl').goal = wanted.goal
- then
- let pf' = List.hd pfl' in
- let spfl = left@(pf'::right) in
- let newstatus = and_status (List.map pf_status spfl) in
- { open_subgoals = newstatus;
- goal = p.goal;
- ref = Some(r,spfl) }
- else
- error "descend: validation"))
- | _ -> assert false)
- else
- error "Too few subproofs"
-
let traverse n pts = match n with
| 0 -> (* go to the parent *)
(match pts.tstack with
| [] -> error "traverse: no ancestors"
| (_,v)::tl ->
- { tpf = v [pts.tpf];
+ let pf = v [pts.tpf] in
+ let pf = norm_evar_proof pts.tpfsigma pf in
+ { tpf = pf;
tstack = tl;
tpfsigma = pts.tpfsigma })
| -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
(match pts.tpf.ref with
- | Some (Tactic (_,spf),_) ->
+ | Some (Nested (_,spf),_) ->
let v = (fun pfl -> pts.tpf) in
{ tpf = spf;
tstack = (-1,v)::pts.tstack;
@@ -718,17 +714,23 @@ let app_tac sigr tac p =
sigr := gll.sigma;
v (List.map leaf gll.it)
-(* solve the nth subgoal with tactic tac *)
-let solve_nth_pftreestate n tac pts =
+(* modify proof state at current position *)
+
+let map_pftreestate f pts =
let sigr = ref pts.tpfsigma in
- let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+ let tpf' = f sigr pts.tpf in
let tpf'' =
- if !sigr == pts.tpfsigma then tpf'
- else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
+ if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
{ tpf = tpf'';
tpfsigma = !sigr;
tstack = pts.tstack }
+(* solve the nth subgoal with tactic tac *)
+
+let solve_nth_pftreestate n tac =
+ map_pftreestate
+ (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
+
let solve_pftreestate = solve_nth_pftreestate 1
(* This function implements a poor man's undo at the current goal.
@@ -880,6 +882,38 @@ let prev_unproven pts =
let rec top_of_tree pts =
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
+let change_rule f pts =
+ let mark_top _ pt =
+ match pt.ref with
+ Some (oldrule,l) ->
+ {pt with ref=Some (f oldrule,l)}
+ | _ -> invalid_arg "change_rule" in
+ map_pftreestate mark_top pts
+
+let match_rule p pts =
+ match (proof_of_pftreestate pts).ref with
+ Some (r,_) -> p r
+ | None -> false
+
+let rec up_until_matching_rule p pts =
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ if match_rule p one_up then
+ pts
+ else
+ up_until_matching_rule p one_up
+
+let rec up_to_matching_rule p pts =
+ if match_rule p pts then
+ pts
+ else
+ if is_top_pftreestate pts then
+ raise Not_found
+ else
+ let one_up = traverse 0 pts in
+ up_to_matching_rule p one_up
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 417ddbcd..d8b13dba 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 7911 2006-01-21 11:18:36Z herbelin $ i*)
+(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*)
(*i*)
open Term
@@ -32,20 +32,17 @@ val apply_sig_tac :
type transformation_tactic = proof_tree -> (goal list * validation)
-val add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val lookup_tactic : string -> (closed_generic_argument list) -> tactic
-
(*s Hiding the implementation of tactics. *)
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
- a single proof node *)
-val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : tactic_expr -> tactic -> tactic
-val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+ a single proof node. The boolean tells if the default tactic is used. *)
+val abstract_operation : compound_rule -> tactic -> tactic
+val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
+val abstract_extended_tactic :
+ ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
val refiner : rule -> tactic
-val vernac_tactic : string * closed_generic_argument list -> tactic
val frontier : transformation_tactic
val list_pf : proof_tree -> goal list
val unTAC : tactic -> goal sigma -> proof_tree sigma
@@ -148,6 +145,12 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
+(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
+ has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
+ Equivalent to [(tac1;try tac2)||tac2] *)
+
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
+
(*s Tactics handling a list of goals. *)
type validation_list = proof_tree list -> proof_tree list
@@ -170,11 +173,14 @@ type pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
+val match_rule : (rule -> bool) -> pftreestate -> bool
val evc_of_pftreestate : pftreestate -> evar_map
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
+val map_pftreestate :
+ (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
@@ -193,6 +199,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate
val next_unproven : pftreestate -> pftreestate
val prev_unproven : pftreestate -> pftreestate
val top_of_tree : pftreestate -> pftreestate
+val match_rule : (rule -> bool) -> pftreestate -> bool
+val up_until_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val up_to_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val change_rule : (rule -> rule) -> pftreestate -> pftreestate
val change_constraints_pftreestate
: evar_map -> pftreestate -> pftreestate
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b721dacd..0fe21552 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 8917 2006-06-07 16:59:05Z herbelin $ i*)
+(*i $Id: tacexpr.ml 9267 2006-10-24 12:55:46Z herbelin $ i*)
open Names
open Topconstr
@@ -234,7 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
| TacExternal of loc * string * string *
('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
- | TacFreshId of string option
+ | TacFreshId of string or_var list
| Tacexp of 'tac
(* Globalized tactics *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 889e06a8..96df8f64 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -31,6 +31,8 @@ type debug_info =
(* An exception handler *)
let explain_logic_error = ref (fun e -> mt())
+let explain_logic_error_no_anomaly = ref (fun e -> mt())
+
(* Prints the goal *)
let db_pr_goal g =
msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index fc1b6120..6de8244d 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 7911 2006-01-21 11:18:36Z herbelin $ i*)
+(*i $Id: tactic_debug.mli 9092 2006-08-28 11:42:14Z bertot $ i*)
open Environ
open Pattern
@@ -66,5 +66,11 @@ val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
(* An exception handler *)
val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+(* For use in the Ltac debugger: some exception that are usually
+ consider anomalies are acceptable because they are caught later in
+ the process that is being debugged. One should not require
+ from users that they report these anomalies. *)
+val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
+
(* Prints a logic failure message for a rule *)
val db_logic_failure : debug_info -> exn -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 02:31:18 +0000