diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-20 12:47:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-20 12:47:39 +0000 |
| commit | 1cda396cb2c92dc0078d74e581a76cdd62b0ee8a (patch) | |
| tree | 7c75ee7a97b6f3a238c97f5c91859fbdd87bbad5 /tactics | |
| parent | 94b5cb2a8a10a7e97e8f63ca85d436e983b959a7 (diff) | |
Globalisation des hints autorewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4678 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a0f0f7226..2aafd3e98 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -65,7 +65,7 @@ let autorewrite tac_main lbas = (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.interp t)) lrl in + let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrl in let l = try List.rev_append l (Stringmap.find rbase !rewtab) @@ -79,8 +79,8 @@ let export_hintrewrite x = Some x let subst_hintrewrite (_,subst,(rbase,list as node)) = let subst_first (cst,b,t as pair) = let cst' = Term.subst_mps subst cst in - todo "substitute tactics in autorewrite hints!"; - if cst == cst' then pair else + let t' = Tacinterp.subst_tactic subst t in + if cst == cst' & t == t' then pair else (cst',b,t) in let list' = list_smartmap subst_first list in @@ -101,4 +101,5 @@ let (in_hintrewrite,out_hintrewrite)= (* To add rewriting rules to a base *) let add_rew_rules base lrul = + let lrul = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.glob_tactic t)) lrul in Lib.add_anonymous_leaf (in_hintrewrite (base,lrul)) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index c2c6bd778..71b377f43 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -109,6 +109,8 @@ val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic +val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr + (* Hides interpretation for pretty-print *) val hide_interp : raw_tactic_expr -> tactic option -> tactic |