From 92b8d5eaa511036a6bc31dfb2d660a97eaf08e2c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Oct 2002 16:30:17 +0000 Subject: [PATCH] hopefully last tactic update cvs log --- helm/gTopLevel/fourierR.ml | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 21f1d5b33..e664bc999 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -664,7 +664,7 @@ let rec filter_real_hyp context cont = [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> ( let n = find_in_context h cont in - [(Cic.Rel(n),t)] @ filter_real_hyp next cont) + [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont ;; @@ -678,23 +678,42 @@ let rec superlift c n= ;; -(* this may not work *) +(* fix !!!!!!!!!! this may not work *) let equality_replace a b = let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;a;b]) ;; -(* unused *) let tcl_fail a ~status:(proof,goal) = match a with - 1 -> raise (ProofEngineTypes.Fail "???????") + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") |_-> (proof,[goal]) ;; +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref (-1) in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; + (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= - proof,[goal] + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) + ~continuation:(Tacticals.then_ + ~start:(Ring.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) ;; (* ********************* TATTICA ******************************** *) -- 2.39.2