X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fring.ml;h=7695a4ff0c82d885b66c9a76f1a3478cd915823b;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=0bc26514d45819ce8e4e2e026edf50c7f765519f;hpb=e00d05ab58597620345c2fd49b84a23efa8db34c;p=helm.git diff --git a/components/tactics/ring.ml b/components/tactics/ring.ml index 0bc26514d..7695a4ff0 100644 --- a/components/tactics/ring.ml +++ b/components/tactics/ring.ml @@ -122,14 +122,14 @@ let cic_is_const ?(uri: uri option = None) term = @param proof a proof @return the uri of a given proof *) -let uri_of_proof ~proof:(uri, _, _, _, _) = uri +let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri (** @param status current proof engine status @raise Failure if proof is None @return current goal's metasenv *) -let metasenv_of_status ((_,m,_,_, _), _) = m +let metasenv_of_status ((_,m,_,_,_, _), _) = m (** @param status a proof engine status @@ -447,7 +447,7 @@ let purge_hyps_tac ~count = (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status)) | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, _) = CicUtil.lookup_meta goal metasenv in let proof',goal' = aux count context status in assert (goal = goal') ; @@ -486,10 +486,10 @@ let ring_tac status = ProofEngineTypes.apply_tactic (Tacticals.first ~tactics:[ - "reflexivity", EqualityTactics.reflexivity_tac ; - "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; - "exact sym_eqt su t1 ...", exact_tac + EqualityTactics.reflexivity_tac ; + exact_tac ~term:t1'_eq_t1'' ; + exact_tac ~term:t2'_eq_t2'' ; + exact_tac ~term:( Cic.Appl [mkConst HelmLibraryObjects.Logic.sym_eq_URI @@ -499,7 +499,7 @@ let ring_tac status = ] ; t1'_eq_t1'' ]) ; - "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status -> + ProofEngineTypes.mk_tactic (fun status -> let status' = (* status after 1st elim_type use *) let context = context_of_status status in let b,_ = (*TASSI : FIXME*) @@ -529,9 +529,8 @@ let ring_tac status = ProofEngineTypes.apply_tactic (Tacticals.first (* try to solve 1st subgoal *) ~tactics:[ - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; - "exact sym_eqt su t2 ...", - exact_tac + exact_tac ~term:t2'_eq_t2''; + exact_tac ~term:( Cic.Appl [mkConst HelmLibraryObjects.Logic.sym_eq_URI @@ -541,7 +540,6 @@ let ring_tac status = ] ; t2'_eq_t2'' ]) ; - "elim_type eqt su t2 ...", ProofEngineTypes.mk_tactic (fun status -> let status' = let context = context_of_status status in