diff options
| author | filliatr | 1999-11-24 08:19:55 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-24 08:19:55 +0000 |
| commit | f9676380178d7af90d8cdf64662866c82139f116 (patch) | |
| tree | 78a9e7e9d79a858d62f89b6efb53be0d05f66457 /proofs | |
| parent | 6c28c8f38c6f47cc772d42e5cc54398785d63bc0 (diff) | |
Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/tacred.mli | 2 |
3 files changed, 5 insertions, 6 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 21fc10bf73..4c14040bdd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -426,9 +426,8 @@ let clenv_val_of clenv mv = (match Intmap.find mv clenv.env with | Cltyp _ -> DOP0(Meta mv) | Clval(b,_) -> - instance (List.map (fun mv' -> (mv',valrec mv')) - (Intset.elements b.freemetas)) - (w_env clenv.hook) (w_Underlying clenv.hook) b.rebus) + plain_instance (List.map (fun mv' -> (mv',valrec mv')) + (Intset.elements b.freemetas)) b.rebus) with Not_found -> DOP0(Meta mv) in @@ -439,7 +438,7 @@ let clenv_instance clenv b = List.map (fun mv -> (mv,clenv_val_of clenv mv)) (Intset.elements b.freemetas) in - instance c_sigma (w_env clenv.hook) (w_Underlying clenv.hook) b.rebus + plain_instance c_sigma b.rebus let clenv_instance_term clenv c = clenv_instance clenv (mk_freelisted c) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index de56125af5..f5daf8b361 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -69,7 +69,7 @@ val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic val clenv_independent : wc clausenv -> constr freelisted * constr freelisted -> int list val clenv_missing : - wc clausenv -> constr freelisted * constr freelisted -> int list + 'a clausenv -> constr freelisted * constr freelisted -> int list val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv val clenv_lookup_name : 'a clausenv -> identifier -> int diff --git a/proofs/tacred.mli b/proofs/tacred.mli index 59069fc046..ccaaae4fb3 100644 --- a/proofs/tacred.mli +++ b/proofs/tacred.mli @@ -9,7 +9,7 @@ open Evd open Reduction (*i*) -(* Reduction functions associated to tactics. *) +(* Reduction functions associated to tactics. \label{tacred} *) val hnf_constr : 'a reduction_function |