From 07ffd30a82ebfe35811ca43d71aeacdb86f4cc87 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 6 Mar 2008 14:56:08 +0000
Subject: Syntax changes in typeclasses, remove "?" for usual implicit
 arguments binding, add "!" syntax for the new binders which require
 parameters and not superclasses. Change backquotes for curly braces for
 user-given implicit arguments, following tradition. This requires a hack a la
 lpar-id-coloneq. Change ident to global for typeclass names in class binders.
 Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C
 t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3992648592..ee5acffd98 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -157,7 +157,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    evar_defs ref -> env -> 
+    evar_defs ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
@@ -667,11 +667,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let evd = nf_evar_defs evd in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
-    let c' = nf_evar (evars_of evd) c' in
       evdref := evd;
-      c'
+      nf_evar (evars_of evd) c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
-- 
cgit v1.2.3