diff options
Diffstat (limited to 'contrib/first-order/rules.ml')
| -rw-r--r-- | contrib/first-order/rules.ml | 44 |
1 files changed, 23 insertions, 21 deletions
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index 7fbefa37..f6653b82 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rules.ml,v 1.24.2.1 2004/07/16 19:30:10 herbelin Exp $ *) +(* $Id: rules.ml 7909 2006-01-21 11:09:18Z herbelin $ *) open Util open Names @@ -57,18 +57,18 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try exact_no_check (constr_of_reference (find_left t seq)) - with Not_found->tclFAIL 0 "No axiom link" + try exact_no_check (constr_of_global (find_left t seq)) + with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= tclIFTHENELSE (try tclTHENLIST - [generalize [mkApp(constr_of_reference id, - [|constr_of_reference (find_left a seq)|])]; + [generalize [mkApp(constr_of_global id, + [|constr_of_global (find_left a seq)|])]; clear_global id; intro] - with Not_found->tclFAIL 0 "No link") + with Not_found->tclFAIL 0 (Pp.str "No link")) (wrap 1 false continue seq) backtrack (* right connectives rules *) @@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [simplest_elim (constr_of_reference id); + [simplest_elim (constr_of_global id); clear_global id; tclDO n intro]) (wrap n false continue seq) @@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls= tclDO n intro; wrap n false continue seq] in tclIFTHENSVELSE - (simplest_elim (constr_of_reference id)) + (simplest_elim (constr_of_global id)) (Array.map f v) backtrack gls let left_false_tac id= - simplest_elim (constr_of_reference id) + simplest_elim (constr_of_global id) (* left arrow connective rules *) @@ -127,7 +127,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in - let head=mkApp ((lift p (constr_of_reference id)),[|capply|]) in + let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in Sign.it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in let newhyps=list_tabulate myterm lp in @@ -141,7 +141,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= let ll_arrow_tac a b c backtrack id continue seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in let d=mkLambda (Anonymous,b, - mkApp ((constr_of_reference id), + mkApp ((constr_of_global id), [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (cut c) @@ -150,7 +150,7 @@ let ll_arrow_tac a b c backtrack id continue seq= clear_global id; wrap 1 false continue seq]; tclTHENS (cut cc) - [exact_no_check (constr_of_reference id); + [exact_no_check (constr_of_global id); tclTHENLIST [generalize [d]; clear_global id; @@ -168,17 +168,19 @@ let forall_tac backtrack continue seq= (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then - tclFAIL 0 "reversible in 1st order mode" + tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack) -let left_exists_tac ind id continue seq gls= +let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in - tclTHENLIST - [simplest_elim (constr_of_reference id); - clear_global id; - tclDO n intro; - (wrap (n-1) false continue seq)] gls + tclIFTHENELSE + (simplest_elim (constr_of_global id)) + (tclTHENLIST [clear_global id; + tclDO n intro; + (wrap (n-1) false continue seq)]) + backtrack + gls let ll_forall_tac prod backtrack id continue seq= tclORELSE @@ -187,7 +189,7 @@ let ll_forall_tac prod backtrack id continue seq= [intro; (fun gls-> let id0=pf_nth_hyp_id gls 1 in - let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in + let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in tclTHEN (generalize [term]) (clear [id0]) gls); clear_global id; intro; @@ -211,4 +213,4 @@ let normalize_evaluables= None->unfold_in_concl (Lazy.force defined_connectives) | Some (id,_,_)-> unfold_in_hyp (Lazy.force defined_connectives) - (id,[],(Tacexpr.InHypTypeOnly,ref None))) + (id,[],Tacexpr.InHypTypeOnly)) |