diff options
| author | herbelin | 2003-01-25 09:48:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-25 09:48:53 +0000 |
| commit | 15fb1a550dd70afe51ff40ba17bbf489cd31f7e8 (patch) | |
| tree | c33af0a4b8f4774dafa1756cb169ffc9e51a5607 | |
| parent | a35f72227565f84c309c057dd9f25229c9a613a5 (diff) | |
Un type "standardisé" pour new_hyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3611 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/hiddentac.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 52661952ef..749a5b12d8 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -56,8 +56,7 @@ let h_new_induction c e idl = abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl) let h_new_destruct c e idl = abstract_tactic (TacNewDestruct (c,e,idl)) (new_destruct c e idl) -let h_specialize n (c,bl as d) = - abstract_tactic (TacSpecialize (n,d)) (new_hyp n c bl) +let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) (* Context management *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bb5ca65012..02c0e65918 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -788,7 +788,7 @@ let rec intros_clearing = function (* Adding new hypotheses *) -let new_hyp mopt c lbind g = +let new_hyp mopt (c,lbind) g = let (wc,kONT) = startWalk g in let clause = make_clenv_binding wc (c,w_type_of wc c) lbind in let (thd,tstack) = whd_stack (clenv_instance_template clause) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0c9744e2c6..3a2ac7b222 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -138,7 +138,7 @@ val pattern_option : (int list * constr) list -> hyp_location option -> tactic val clear : identifier list -> tactic val clear_body : identifier list -> tactic -val new_hyp : int option ->constr -> constr substitution -> tactic +val new_hyp : int option -> constr with_bindings -> tactic val move_hyp : bool -> identifier -> identifier -> tactic val rename_hyp : identifier -> identifier -> tactic |