diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-01 11:21:33 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-01 11:21:33 +0000 |
| commit | bbae07b156c9134bbfffcad4c6912536c3eb416a (patch) | |
| tree | dae6ad1112ab64fc57e4a892cbbd706bf53ef305 /tactics/tactics.ml | |
| parent | d383d81326659586dd7f18f768fc9355deae3208 (diff) | |
labels appliques dans un ordre incorrect
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2504 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d6ab27572..2fb555d88 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -753,7 +753,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl = (d,List.exists (fun((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt) in d'::ctxt in - let ctxt' = fold_named_context compute_dependency ~init:[] env in + let ctxt' = fold_named_context compute_dependency env ~init:[] in let compute_marks ((depdecls,marks as accu),lhyp) ((hyp,_,_) as d,b) = if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp) else (accu, Some hyp) in |