diff options
| author | herbelin | 2000-10-03 18:13:02 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-03 18:13:02 +0000 |
| commit | e7a935fc13fca079b4ee64ace19029851c01eaf9 (patch) | |
| tree | 61ae98385011cb897488927d7790865655294ca2 /dev | |
| parent | 265365329632320e3880e792712c8223c1cb1316 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@641 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index 7aeda57a7b..c2b12d2175 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -57,6 +57,10 @@ Changements dans les fonctions : map2_vect -> array_map2 list_of_tl_vect -> array_list_of_tl + Names + sign_it -> fold_var_context (se fait sur env maintenant) + it_sign -> fold_var_context_reverse (sur env maintenant) + Generic noccur_bet -> noccur_between substn_many -> substnl @@ -105,6 +109,7 @@ Changements dans les fonctions : pf_constr_of_com_sort -> pf_interp_type pf_constr_of_com -> pf_interp_constr pf_get_hyp -> pf_get_hyp_typ + pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant) Pattern raw_sopattern_of_compattern -> Astterm.interp_constrpattern @@ -114,6 +119,8 @@ Changements dans les fonctions : Tacticals matches -> gl_is_matching dest_match -> gl_matches + suff -> utiliser sort_of_goal + lookup_eliminator -> utiliser sort_of_goal pour le dernier arg Divers initial_sign -> var_context |