- 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

2 files changed, 12 insertions, 9 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 2e057e438b..d98788eede 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -16,6 +16,7 @@ open Nametab
 open Rawterm
 open Topconstr
 open Term
+open Evd
 
 type argument_type =
   (* Basic types *)
@@ -47,6 +48,10 @@ type 'a and_short_name = 'a * identifier located option
 type 'a or_by_notation = AN of 'a | ByNotation of loc * string
 
 type rawconstr_and_expr = rawconstr * constr_expr option
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
+
+type 'a with_ebindings = 'a * open_constr bindings
 
 (* Dynamics but tagged by a type expression *)
 
@@ -56,7 +61,7 @@ let dyntab = ref ([] : string list)
 
 type rlevel = constr_expr
 type glevel = rawconstr_and_expr
-type tlevel = constr
+type tlevel = open_constr
 
 type ('a,'b) abstract_argument_type = argument_type
 
@@ -90,10 +95,6 @@ and pr_case_intro_pattern = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
 
-type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = unit * constr_expr
-type open_rawconstr = unit * rawconstr_and_expr
-
 let rawwit_bool = BoolArgType
 let globwit_bool = BoolArgType
 let wit_bool = BoolArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index db078bfc1e..ccaf93d58c 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -15,6 +15,7 @@ open Libnames
 open Rawterm
 open Topconstr
 open Term
+open Evd
 
 type 'a and_short_name = 'a * identifier located option
 
@@ -25,10 +26,11 @@ type 'a or_by_notation = AN of 'a | ByNotation of loc * string
 (* The [constr_expr] field is [None] in TacDef though *)
 type rawconstr_and_expr = rawconstr * constr_expr option
 
-type open_constr = Evd.evar_map * Term.constr
 type open_constr_expr = unit * constr_expr
 type open_rawconstr = unit * rawconstr_and_expr
 
+type 'a with_ebindings = 'a * open_constr bindings
+
 type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
   | IntroWildcard
@@ -106,7 +108,7 @@ ExtraArgType of string         '_a                      '_b
 
 type rlevel = constr_expr
 type glevel = rawconstr_and_expr
-type tlevel = constr
+type tlevel = open_constr
 
 type ('a,'co) abstract_argument_type
 
@@ -176,11 +178,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
 
 val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,tlevel) abstract_argument_type
+val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type
 
 val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
 val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
-val wit_bindings : (constr bindings,tlevel) abstract_argument_type
+val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type
 
 val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type