diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 17:14:02 +0000 |
| commit | 85fb5f33b1cac28e1fe4f00741c66f6f58109f84 (patch) | |
| tree | 4913998a925cb148c74a607bf7523ae1d28853ce /proofs/tacmach.ml | |
| parent | 31ebb89fe48efe92786b1cddc3ba62e7dfc4e739 (diff) | |
premiere reorganisation de l\'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index ceb22229c..1b1e88e82 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -14,7 +14,6 @@ open Nameops open Sign open Term open Termops -open Instantiate open Environ open Reductionops open Evd @@ -32,7 +31,7 @@ let re_sig it gc = { it = it; sigma = gc } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -91,10 +90,6 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_execute gls = - let evc = project gls in - Typing.unsafe_machine (pf_env gls) evc - let pf_reduction_of_redexp gls re c = reduction_of_redexp re (pf_env gls) (project gls) c |