diff options
| author | herbelin | 2004-03-27 12:19:23 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-27 12:19:23 +0000 |
| commit | ed149bd9f177041c78b4d9da28dc53dfe1a7fa59 (patch) | |
| tree | 76a30c9bdb6dd4087f46bff5a375c938a386381e /toplevel/metasyntax.ml | |
| parent | 264658d653e4c12b1739504f898f136396fb8ea4 (diff) | |
Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajout de la prise en compte dynamique des arguments scope pour les inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5586 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c4d8bce9e2..a3415cbaa9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1199,8 +1199,7 @@ let add_notation_interpretation df names c sc = check_notation_existence (make_notation_key symbs); let (acvars,ac) = interp_aconstr names vars c in let a = (remove_vars recs acvars,ac) (* For recursive parts *) in - let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c - in + let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in let for_oldpp = set_data_for_v7_pp recs a_for_old vars in add_notation_interpretation_core false symbs for_oldpp df a sc false false |