diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-31 19:02:36 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-31 19:02:36 +0000 |
| commit | 61bf07f5a58260db287696def58dba1aeac84a81 (patch) | |
| tree | 8619ac1f822b853913c376ca47c2ca21a033bc0e /tactics | |
| parent | c1db8eb695a04d172130959ff38eef61d3ca9653 (diff) | |
Mise en place de la possibilite d'unfolder des variables locales et des constantes qualifiees
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1301 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 8 |
2 files changed, 7 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1080b9509..f532166d0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -222,8 +222,8 @@ let dyn_reduce = function (* Unfolding occurrences of a constant *) let unfold_constr = function - | ConstRef sp -> unfold_in_concl [[],sp] - | VarRef sp -> unfold_in_concl [[],sp] + | ConstRef sp -> unfold_in_concl [[],Closure.EvalConstRef sp] + | VarRef sp -> unfold_in_concl [[],Closure.EvalVarRef (basename sp)] | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">] (*******************************************) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9caeafde6..3d5cf9bad 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -116,11 +116,13 @@ val simpl_option : identifier option -> tactic val normalise_in_concl: tactic val normalise_in_hyp : identifier -> tactic val normalise_option : identifier option -> tactic -val unfold_in_concl : (int list * section_path) list -> tactic +val unfold_in_concl : (int list * Closure.evaluable_global_reference) list + -> tactic val unfold_in_hyp : - (int list * section_path) list -> identifier -> tactic + (int list * Closure.evaluable_global_reference) list -> identifier -> tactic val unfold_option : - (int list * section_path) list -> identifier option -> tactic + (int list * Closure.evaluable_global_reference) list -> identifier option + -> tactic val reduce : red_expr -> identifier list -> tactic val dyn_reduce : tactic_arg list -> tactic val dyn_change : tactic_arg list -> tactic |