diff options
| author | Hugo Herbelin | 2014-11-08 12:36:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-08 16:17:09 +0100 |
| commit | 4f2bbf0c82f8ea4ba26990770fb1f103a6ca1668 (patch) | |
| tree | 155b33821acfd18702fcd5daffa0802b2d2b4fe9 /tactics | |
| parent | 34d52eb3577fa329e4637409e8d602fd23ac126d (diff) | |
Compatibility with 8.4 in the heuristic used to build the induction
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 599d42ee49..d1ab3cb38e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2742,7 +2742,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let hd,argl = decompose_app indtyp in let params = List.firstn nparams argl in (* le gl est important pour ne pas préévaluer *) - let rec atomize_one i args = + let rec atomize_one i params args = if Int.equal i nparams then let t = applist (hd, params @ List.map mkVar args) in Proofview.V82.tactic @@ -2753,7 +2753,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = | Var id when not (List.mem id args) && not (List.exists (occur_var env id) params) -> (* We know that the name can be cleared after destruction *) - atomize_one (i-1) (id::args) + atomize_one (i-1) params (id::args) | _ -> let id = match kind_of_term c with | Var id -> id @@ -2763,9 +2763,9 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let x = fresh_id_in_env args id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) (x::args)) + (atomize_one (i-1) (List.map (replace_term c (mkVar x)) params) (x::args)) in - atomize_one (List.length argl) [] + atomize_one (List.length argl) params [] end let find_atomic_param_of_ind nparams indtyp = |