- Propagation des evars non résolues vers les with_bindings; permet par exemple

  de résoudre des buts comme celui-ci :

  Record nat_retract : Type := 
    {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
  Goal nat_retract.
  exists (fun x => x) (fun x => x).

- Nouvelle tentative d'utilisation des types des metas/evars pour
  inférer de nouvelles instances de metas/evars; permet par exemple
  d'utiliser f_equal sans option with, mais aussi, avec la modif
  précédente, de résoudre des buts tels que

  Goal exists f:bool->Prop, f true = True.
  exists (fun x => True).

  [Les expériences passées avaient montré qu'en prenant en compte les
  types dans l'unification, on peut unifier trop tôt une evars à une
  mauvaise sorte; à défaut de mécanisme de prise en compte des problème
  d'unification avec sous-typage, on s'est interdit ici d'unifier des
  types qui sont des arités.]

- Tout les constr de tactic_expr deviennent des open_constr (même si seul
  with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index df078f3028..307e0af231 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -48,10 +48,16 @@ let pr_lconstr_env_at_top env = pr_lconstr_core true env
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
 
+let pr_open_lconstr_env env (_,c) = pr_lconstr_env env c
+let pr_open_constr_env env (_,c) = pr_constr_env env c
+
   (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
 let pr_lconstr t = pr_lconstr_env (Global.env()) t
 let pr_constr t = pr_constr_env (Global.env()) t
 
+let pr_open_lconstr (_,c) = pr_lconstr c
+let pr_open_constr (_,c) = pr_constr c
+
 let pr_type_core at_top env t =
   pr_constr_expr (extern_type at_top env t)
 let pr_ltype_core at_top env t =