diff options
| author | bertot | 2006-08-17 13:42:36 +0000 |
|---|---|---|
| committer | bertot | 2006-08-17 13:42:36 +0000 |
| commit | c7446212657af6c407b95736b4fe13c6e26d5690 (patch) | |
| tree | 913740b690073241448511b4b6af0a29d23442c4 | |
| parent | fc37b6ea9f7cfb26e62b5cb95973f1a9ab52284a (diff) | |
corrects an error in the substitution of module paths inside tactics:
objects of the form TacDynamic should not be left unchanged if their content
is tagged with "constr". This correction makes that setoid ring can
now work with rings that were declared inside a module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b83e590f9a..20649674d6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2170,9 +2170,11 @@ and subst_tacarg subst = function TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) - | TacDynamic(_,t) as x -> + | TacDynamic(the_loc,t) as x -> (match tag t with - | "tactic" | "value" | "constr" -> x + | "tactic" | "value" -> x + | "constr" -> + TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) | s -> anomaly_loc (dloc, "Tacinterp.val_interp", str "Unknown dynamic: <" ++ str s ++ str ">")) |