diff options
| author | filliatr | 1999-12-01 08:03:06 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-01 08:03:06 +0000 |
| commit | dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 (patch) | |
| tree | 21bd3b1535e2e9b9cfcfa0f8cab47817a1769b70 /proofs/logic.ml | |
| parent | 8b882c1ab5a31eea35eec89f134238dd17b945c2 (diff) | |
- Typing -> Safe_typing
- proofs/Typing_ev -> pretyping/Typing
- env -> sign
- fonctions var_context
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b0823c1b2d..f89c6e9b4e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -10,7 +10,7 @@ open Term open Sign open Environ open Reduction -open Typing_ev +open Typing open Proof_trees open Typeops open Coqast @@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto = let prim_refiner r sigma goal = let env = goal.evar_env in - let sign = get_globals (context env) in + let sign = var_context env in let cl = goal.evar_concl in let info = goal.evar_info in match r with @@ -401,8 +401,8 @@ let prim_refiner r sigma goal = | _ -> anomaly "prim_refiner: Unrecognized primitive rule" let abst_value c = - let env = Global.env () in - Environ.abst_value (Typing.unsafe_env_of_env env) c + let env = Global.unsafe_env () in + Environ.abst_value env c let extract_constr = let rec crec vl = function |