hopefully last tactic update cvs log

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 21f1d5b33d5d2edcab362d3c4df87972c3009850..e664bc999deaf5400e60524561204106fba36051 100644 (file)
--- 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 ******************************** *)