diff options
| author | barras | 2002-02-15 18:02:05 +0000 |
|---|---|---|
| committer | barras | 2002-02-15 18:02:05 +0000 |
| commit | 1e6c3e993fd33d01713aae34a8cefbc210b3898a (patch) | |
| tree | 2f8e2aba2c50587146ac4100bb8bf3c426fca65f /kernel/safe_typing.ml | |
| parent | 0eff88d5a9ad9279a4e68fdb6e210c6ea671b613 (diff) | |
petits changements cosmetiques sur les tactiques
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses
definies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f96ff1fd99..f284d774d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -54,7 +54,7 @@ let push_rel_or_named_def push (id,b,topt) env = let env'' = push (id,Some j.uj_val,typ) env' in (cst,env'') -let push_named_def = push_rel_or_named_def push_named_decl +let push_named_def = push_rel_or_named_def push_named let push_rel_def = push_rel_or_named_def push_rel let push_rel_or_named_assum push (id,t) env = @@ -64,7 +64,7 @@ let push_rel_or_named_assum push (id,t) env = let env'' = push (id,None,t) env' in (cst,env'') -let push_named_assum = push_rel_or_named_assum push_named_decl +let push_named_assum = push_rel_or_named_assum push_named let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env) let push_rels_with_univ vars env = @@ -126,7 +126,7 @@ let add_constraints = Environ.add_constraints let rec pop_named_decls idl env = match idl with | [] -> env - | id::l -> pop_named_decls l (Environ.pop_named_decl id env) + | id::l -> pop_named_decls l (Environ.pop_named id env) let export = export let import = import |