diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f0d4dc51..11625cbd 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacticals.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -23,7 +21,7 @@ open Refiner open Tacmach open Clenv open Clenvtac -open Rawterm +open Glob_term open Pattern open Matching open Genarg @@ -61,8 +59,9 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO -let tclPROGRESS = Refiner.tclPROGRESS +let tclTIMEOUT = Refiner.tclTIMEOUT let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS +let tclPROGRESS = Refiner.tclPROGRESS let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL let tclTHENTRY = Refiner.tclTHENTRY let tclIFTHENELSE = Refiner.tclIFTHENELSE @@ -173,12 +172,9 @@ let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl -let onAllHypsAndConclLR tac gl = tclMAP tac (List.rev (fullGoal gl)) gl let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl -let tryAllHypsAndConclLR tac gl = - tclFIRST_PROGRESS_ON tac (List.rev (fullGoal gl)) gl let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls @@ -292,7 +288,7 @@ let compute_construtor_signatures isrec (_,k as ity) = | Prod (_,_,c), recarg::rest -> let b = match dest_recarg recarg with | Norec | Imbr _ -> false - | Mrec j -> isrec & j=k + | Mrec (_,j) -> isrec & j=k in b :: (analrec c rest) | LetIn (_,_,_,c), rest -> false :: (analrec c rest) | _, [] -> [] @@ -367,7 +363,8 @@ let general_elim_then_using mk_elim match predicate with | None -> elimclause' | Some p -> - clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause' + clenv_unify ~flags:Unification.elim_flags + Reduction.CONV (mkMeta pmv) p elimclause' in elim_res_pf_THEN_i elimclause' branchtacs gl |