diff options
| author | ppedrot | 2013-06-22 15:33:40 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-22 15:33:40 +0000 |
| commit | d33f10ce6dfc689da768f23360d46b88a57fc42e (patch) | |
| tree | 841db99fd21157948d3227cefc2afa67e856b839 | |
| parent | 34e80b356fcccd938f114925e91c53cb33b2bd19 (diff) | |
Fixing the semantics of the previous patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16603 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 852348e71e..027429b363 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -399,7 +399,7 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } = (* Extract the constr list from lfun *) let extract_ltac_constr_values ist env = - let fold (vars1, vars2) (id, v) = + let fold (id, v) (vars1, vars2) = try let c = coerce_to_constr env v in (Id.Map.add id c vars1, vars2) @@ -414,7 +414,7 @@ let extract_ltac_constr_values ist env = in (vars1, Id.Map.add id ido vars2) in - List.fold_left fold (Id.Map.empty, Id.Map.empty) ist.lfun + List.fold_right fold ist.lfun (Id.Map.empty, Id.Map.empty) (* Extract the identifier list from lfun: join all branches (what to do else?)*) let rec intropattern_ids (loc,pat) = match pat with |