diff options
| author | msozeau | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /contrib/subtac/eterm.ml | |
| parent | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff) | |
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/eterm.ml')
| -rw-r--r-- | contrib/subtac/eterm.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 99727e5f25..66a2b36019 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -96,7 +96,7 @@ let eterm evm t = y' :: l) [] evl in - let t' = (* Substitute evar refs in the term to De Bruijn indices *) + let t' = (* Substitute evar refs in the term by De Bruijn indices *) subst_evars evts 0 t in let t'' = @@ -106,8 +106,6 @@ let eterm evm t = mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)), c, acc)) t' evts - - in let _declare_evar (id, c) = let id = id_of_string ("Evar" ^ string_of_int id) in @@ -120,8 +118,8 @@ let eterm evm t = in msgnl (str "Term constructed in Eterm" ++ Termops.print_constr_env (Global.env ()) t''); - Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts) - + Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts) + open Tacmach let etermtac (evm, t) = eterm evm t |