- (* si le but est une inéquation, on introduit son contraire,
- et le but à prouver devient False *)
-
- try (let tac =
- match ty with
- Cic.Appl ( Cic.Const(u,boh)::args) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |_->assert false)
- |_->assert false
- in tac (proof,goal) )
- with _ ->
-
- (* les hypothèses *)
+
+ (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
+ so let's parse our thesis *)
+
+ let th_to_appl = ref _Rfourier_not_le_gt in
+ (match s_ty with
+ Cic.Appl ( Cic.Const(u,boh)::args) ->
+ (match UriManager.string_of_uri u with
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
+ |_-> failwith "fourier can't be applyed")
+ |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
+
+ (* now let's change our thesis applying the th and put it with hp *)
+
+ let proof,gl = Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
+ ~status:(s_proof,s_goal) in
+ let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
+
+ debug ("port la tesi sopra e la nego. contesto :\n");
+ debug_pcontext s_context;
+
+ (* now we have all the right environment *)
+
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+
+ (* now we want to convert hp to inequations, but first we must lift
+ everyting to thesis level, so that a variable has the save Rel(n)
+ in each hp ( needed by ineq1_of_term ) *)