Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses

........
  r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Comment grammar error
........
  r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
  
  The initial Type Classes patch.
  This patch introduces type classes and instance definitions a la Haskell.
  Technically, it uses the implicit arguments mechanism which was extended a bit. 
  The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
  It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). 
........
  r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix interface
........
  r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix more xlate code
........
  r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
  r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Bug fixes in Instance decls.
........
  r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
  
  Streamline typeclass context implementation, prepare for class binders in proof statements.
........
  r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
  
  Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
  r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
  
  Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
  r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
  
  Stupid bug
........
  r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
  r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
  r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
  
  Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
  New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
  Other bugs related to naming in typeclasses fixed. 
........
  r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
  
  Progress on setoids using type classes, recognize setoid equalities in hyps better.
  Streamline implementation to return more information when resolving setoids (return the results setoid).
........
  r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
  
  Syntax change, more like Coq
........
  r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
  
  Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
  r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
  
  Work on type classes based rewrite tactic.
........
  r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
  
  Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
  r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
  
  Forgot to add a file
........
  r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
  
  Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and 
  implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
  r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
  
  Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. 
  Add useful tactics to Program.Subsets.
........


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

6 files changed, 289 insertions, 32 deletions

diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
new file mode 100644
index 0000000000..0c8bdd2980
--- /dev/null
+++ b/tactics/class_setoid.ml4
@@ -0,0 +1,224 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: eauto.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Reduction
+open Proof_type
+open Proof_trees
+open Declarations
+open Tacticals
+open Tacmach
+open Evar_refiner
+open Tactics
+open Pattern
+open Clenv
+open Auto
+open Rawterm
+open Hiddentac
+open Typeclasses
+open Typeclasses_errors
+
+let e_give_exact c gl = 
+  let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+  if occur_existential t1 or occur_existential t2 then 
+     tclTHEN (Clenvtac.unify t1) (exact_check c) gl
+  else exact_check c gl
+
+let assumption id = e_give_exact (mkVar id)
+
+let morphism_class = lazy (class_info (id_of_string "Morphism"))
+let morphism2_class = lazy (class_info (id_of_string "BinaryMorphism"))
+let morphism3_class = lazy (class_info (id_of_string "TernaryMorphism"))
+
+let get_respect cl = 
+  Option.get (List.hd (Recordops.lookup_projections cl.cl_impl))
+
+let respect_proj = lazy (get_respect (Lazy.force morphism_class))
+let respect2_proj = lazy (get_respect (Lazy.force morphism2_class))
+let respect3_proj = lazy (get_respect (Lazy.force morphism3_class))
+
+let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s
+let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
+let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
+let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
+
+let iff_setoid = lazy (gen_constant ["Classes"; "Setoid"] "iff_setoid")
+let setoid_equiv = lazy (gen_constant ["Classes"; "Setoid"] "equiv")
+let setoid_morphism = lazy (gen_constant ["Classes"; "Setoid"] "setoid_morphism")
+let setoid_refl_proj = lazy (gen_constant ["Classes"; "Setoid"] "equiv_refl")
+  
+let arrow_morphism a b = 
+  mkLambda (Name (id_of_string "A"), a, 
+	   mkLambda (Name (id_of_string "B"), b, 
+		    mkProd (Anonymous, mkRel 2, mkRel 2)))
+    
+let setoid_refl l sa x = 
+  applistc (Lazy.force setoid_refl_proj) (l @ [sa ; x])
+      
+let class_one = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
+let class_two = lazy (Lazy.force morphism2_class, Lazy.force respect2_proj)
+let class_three = lazy (Lazy.force morphism3_class, Lazy.force respect3_proj)
+
+exception Found of (constr * constant * constr list * int * constr * constr array *
+		       (constr * (constr * constr * constr * constr * constr)) option array)
+
+let resolve_morphism_evd env evd app = 
+  let ev = Evarutil.e_new_evar evd env app in
+  let evd' = resolve_typeclasses ~check:false env (Evd.evars_of !evd) !evd in
+  let evm' = Evd.evars_of evd' in
+    match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with
+	Evd.Evar_empty -> raise Not_found
+      | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; c
+
+let is_equiv env sigma t = 
+  isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
+
+let resolve_morphism env sigma direction oldt m args args' = 
+  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let morph_instance, proj, subst, len, m', args, args' = 
+    if is_equiv env sigma m then 
+      let params, rest = array_chop 3 args in
+      let a, r, s = params.(0), params.(1), params.(2) in
+      let params', rest' = array_chop 3 args' in
+      let inst = mkApp (Lazy.force setoid_morphism, params) in
+	(* Equiv gives a binary morphism *)
+      let (cl, proj) = Lazy.force class_two in
+      let ctxargs = [ a; r; a; r; mkProp; Lazy.force iff; s; s; Lazy.force iff_setoid; ] in
+      let m' = mkApp (m, [| a; r; s |]) in
+	inst, proj, ctxargs, 6, m', rest, rest'
+    else
+      let cls =
+	match Array.length args with
+	    1 -> [Lazy.force class_one, 1]
+	  | 2 -> [Lazy.force class_two, 2; Lazy.force class_one, 1]
+	  | 3 -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1]
+	  | n -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1]
+      in
+	try 
+	  List.iter (fun ((cl, proj), n) ->
+	    evars := Evd.create_evar_defs Evd.empty;
+	    let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] cl.cl_context in
+	    let len = List.length ctxevs in
+	    let superevs = substitution_of_named_context evars env cl.cl_name len ctxevs cl.cl_super in
+	    let morphargs, morphobjs = array_chop (Array.length args - n) args in
+	    let morphargs', morphobjs' = array_chop (Array.length args - n) args' in
+	    let args = List.rev_map (fun (_, c) -> c) superevs in
+	    let appm = mkApp(m, morphargs) in
+	    let appmtype = Typing.type_of env sigma appm in
+	    let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in
+	    let mtype = replace_vars superevs (pi3 (List.hd cl.cl_params)) in
+	      try 
+		evars := Unification.w_unify true env CONV ~mod_delta:true appmtype mtype !evars;
+		evars := Evarutil.nf_evar_defs !evars;
+		let app = Evarutil.nf_isevar !evars app in
+		  raise (Found (resolve_morphism_evd env evars app, proj, args, len, appm, morphobjs, morphobjs'))
+	      with Not_found -> ()
+		| Stdpp.Exc_located (_, Pretype_errors.PretypeError _) 
+		| Pretype_errors.PretypeError _ -> ())
+	    cls; 
+	  raise Not_found
+	with Found x -> x
+  in 
+  evars := Evarutil.nf_evar_defs !evars;
+  let evm = Evd.evars_of !evars in
+  let ctxargs = List.map (Reductionops.nf_evar evm) subst in
+  let ctx, sup = Util.list_chop len ctxargs in
+  let m' = Reductionops.nf_evar evm m' in
+  let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in
+  let projargs, respars, ressetoid, typeargs = 
+    array_fold_left2 
+      (fun (acc, ctx, sup, typeargs') x y -> 
+	let par, ctx = list_chop 2 ctx in
+	let setoid, sup = List.hd sup, List.tl sup in
+	  match y with
+	      None ->
+		let refl_proof = setoid_refl par setoid x in
+		  [ refl_proof ; x ; x ] @ acc, ctx, sup, x :: typeargs'
+	    | Some (p, (_, _, _, _, t')) ->
+		if direction then
+		  [ p ; t'; x ] @ acc, ctx, sup, t' :: typeargs'
+		else [ p ; x; t' ] @ acc, ctx, sup, t' :: typeargs')
+      ([], ctx, sup, []) args args'
+  in
+  let proof = applistc appproj (List.rev projargs) in
+  let newt = applistc m' (List.rev typeargs) in
+    match respars, ressetoid with
+	[ a ; r ], [ s ] -> (proof, (a, r, s, oldt, newt))
+      | _ -> assert(false)
+      
+let build_new gl env setoid direction origt newt hyp hypinfo concl =
+  let rec aux t = 
+    match kind_of_term t with
+      | _ when eq_constr t origt -> 
+	  Some (hyp, hypinfo)
+      | App (m, args) ->
+	  let args' = Array.map aux args in
+	    if array_for_all (fun x -> x = None) args' then None
+	    else 
+	      (try Some (resolve_morphism env (project gl) direction t m args args')
+		with Not_found -> None)
+      | Prod (_, x, b) -> 
+	  let x', b' = aux x, aux b in
+	    if x' = None && b' = None then None
+	    else 
+	      (try Some (resolve_morphism env (project gl) direction t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |])
+		with Not_found -> None)
+		
+      | _ -> None
+  in aux concl
+
+let decompose_setoid_eqhyp env sigma c dir t = 
+  match kind_of_term t with
+    | App (equiv, [| a; r; s; x; y |]) ->
+	if dir then (c, (a, r, s, x, y))
+	else (c, (a, r, s, y, x))
+    | App (r, args) when Array.length args >= 2 -> 
+	(try 
+	    let (p, (a, r, s, _, _)) = resolve_morphism env sigma dir t r args (Array.map (fun _ -> None) args) in
+	    let _, args = array_chop (Array.length args - 2) args in
+	      if dir then (c, (a, r, s, args.(0), args.(1)))
+	      else (c, (a, r, s, args.(1), args.(0)))
+	  with Not_found -> error "Not a (declared) setoid equality")
+    | _ -> error "Not a setoid equality"
+
+let cl_rewrite c left2right gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let hyp = pf_type_of gl c in
+  let hypt, (typ, rel, setoid, origt, newt as hypinfo) = decompose_setoid_eqhyp env sigma c left2right hyp in
+  let concl = pf_concl gl in
+  let _concltyp = pf_type_of gl concl in
+  let eq = build_new gl env setoid left2right origt newt hypt hypinfo concl in
+    match eq with  
+	Some (p, (_, _, _, _, t)) -> 
+	  let proj = 
+	    if left2right then 
+	      applistc (Lazy.force coq_proj2)
+		[ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
+	    else 
+	      applistc (Lazy.force coq_proj1)
+		[ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
+	  in
+	    (Tactics.apply proj) gl
+      | None -> tclIDTAC gl
+	  
+open Extraargs
+
+TACTIC EXTEND class_rewrite
+| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite c o ]
+END
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 771dbe7363..b33fbde8aa 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -182,17 +182,17 @@ let interp_constr_or_thesis check_sort sigma env = function
 
 let type_tester_var body typ = 
   raw_app(dummy_loc,
-       RLambda(dummy_loc,Anonymous,typ,
+       RLambda(dummy_loc,Anonymous,Explicit,typ,
 	       RSort (dummy_loc,RProp Null)),body)
 
 let abstract_one_hyp inject h raw = 
   match h with 
       Hvar (loc,(id,None)) ->  
-	RProd (dummy_loc,Name id, RHole (loc,Evd.BinderType (Name id)), raw)
+	RProd (dummy_loc,Name id, Explicit, RHole (loc,Evd.BinderType (Name id)), raw)
     | Hvar (loc,(id,Some typ)) ->  
-	RProd (dummy_loc,Name id,fst typ, raw)
+	RProd (dummy_loc,Name id, Explicit, fst typ, raw)
     | Hprop st -> 
-	RProd (dummy_loc,st.st_label,inject st.st_it, raw)
+	RProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw)
 
 let rawconstr_of_hyps inject hyps head = 
   List.fold_right (abstract_one_hyp inject) hyps head
@@ -254,18 +254,18 @@ let rec raw_of_pat =
 let prod_one_hyp = function
     (loc,(id,None)) ->
       (fun raw ->  
-	 RProd (dummy_loc,Name id, 
+	 RProd (dummy_loc,Name id, Explicit,
 		RHole (loc,Evd.BinderType (Name id)), raw))
   | (loc,(id,Some typ)) -> 
       (fun raw ->  
-	 RProd (dummy_loc,Name id,fst typ, raw))
+	 RProd (dummy_loc,Name id, Explicit, fst typ, raw))
 
 let prod_one_id (loc,id) raw =
-  RProd (dummy_loc,Name id,
+  RProd (dummy_loc,Name id, Explicit,
 	 RHole (loc,Evd.BinderType (Name id)), raw)
 
 let let_in_one_alias (id,pat) raw =
-  RLetIn (dummy_loc,Name id,raw_of_pat pat, raw)
+  RLetIn (dummy_loc,Name id, raw_of_pat pat, raw)
 
 let rec bind_primary_aliases map pat =
   match pat with 
@@ -417,11 +417,11 @@ let interp_casee sigma env = function
 let abstract_one_arg = function
     (loc,(id,None)) ->
       (fun raw ->  
-	 RLambda (dummy_loc,Name id, 
+	 RLambda (dummy_loc,Name id, Explicit, 
 		RHole (loc,Evd.BinderType (Name id)), raw))
   | (loc,(id,Some typ)) -> 
       (fun raw ->  
-	 RLambda (dummy_loc,Name id,fst typ, raw))
+	 RLambda (dummy_loc,Name id, Explicit, fst typ, raw))
 
 let rawconstr_of_fun args body = 
   List.fold_right abstract_one_arg args (fst body)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3211cc6cf1..dbb4648bc8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2579,22 +2579,32 @@ let bad_tactic_args s =
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := Gmap.add kn td !mactab
 
+type tacdef_kind = | NewTac of identifier
+		   | UpdateTac of ltac_constant
+
 let load_md i ((sp,kn),defs) =
   let dp,_ = repr_path sp in
   let mp,dir,_ = repr_kn kn in
   List.iter (fun (id,t) -> 
-    let sp = Libnames.make_path dp id in
-    let kn = Names.make_kn mp dir (label_of_id id) in
-    Nametab.push_tactic (Until i) sp kn;
-    add (kn,t)) defs
-
+    match id with
+	NewTac id ->
+	  let sp = Libnames.make_path dp id in
+	  let kn = Names.make_kn mp dir (label_of_id id) in
+	    Nametab.push_tactic (Until i) sp kn;
+	    add (kn,t)
+      | UpdateTac kn ->
+	  add (kn,t)) defs
+    
 let open_md i((sp,kn),defs) =
   let dp,_ = repr_path sp in
   let mp,dir,_ = repr_kn kn in
   List.iter (fun (id,t) -> 
-    let sp = Libnames.make_path dp id in
-    let kn = Names.make_kn mp dir (label_of_id id) in
-    Nametab.push_tactic (Exactly i) sp kn) defs
+    match id with
+	NewTac id ->
+	  let sp = Libnames.make_path dp id in
+	  let kn = Names.make_kn mp dir (label_of_id id) in
+	    Nametab.push_tactic (Exactly i) sp kn
+      | UpdateTac kn -> ()) defs
 
 let cache_md x = load_md 1 x
 
@@ -2622,27 +2632,40 @@ let print_ltac id =
     (pr_qualid id ++ spc() ++ str "is not a user defined tactic")
 
 (* Adds a definition for tactics in the table *)
-let make_absolute_name (loc,id) =
-  let kn = Lib.make_kn id in
-  if Gmap.mem kn !mactab or is_atomic_kn kn then
+let make_absolute_name (loc,id) repl =
+  try 
+    let kn = if repl then Nametab.locate_tactic (make_short_qualid id) else Lib.make_kn id in
+      if Gmap.mem kn !mactab then
+	if repl then kn
+	else
+	  user_err_loc (loc,"Tacinterp.add_tacdef",
+		       str "There is already an Ltac named " ++ pr_id id)
+      else if is_atomic_kn kn then 
+	user_err_loc (loc,"Tacinterp.add_tacdef",
+		     str "Reserved Ltac name " ++ pr_id id)
+      else kn
+  with Not_found ->
     user_err_loc (loc,"Tacinterp.add_tacdef",
-      str "There is already an Ltac named " ++ pr_id id);
-  kn
-
+		 str "There is no Ltac named " ++ pr_id id)
+      
 let add_tacdef isrec tacl =
 (*  let isrec = if !Flags.p1 then isrec else true in*)
-  let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
+  let rfun = List.map (fun ((loc,id as locid),b,_) -> (id,make_absolute_name locid b)) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
   let gtacl =
-    List.map (fun ((_,id),def) ->
-      (id,Flags.with_option strict_check (intern_tactic ist) def))
-      tacl in
+    List.map2 (fun ((_,id),b,def) (_, qid) ->
+      let k = if b then UpdateTac qid else NewTac id in
+      let t = Flags.with_option strict_check (intern_tactic ist) def in
+	(k, t))
+      tacl rfun in
   let id0 = fst (List.hd rfun) in
   let _ = Lib.add_leaf id0 (inMD gtacl) in
   List.iter
-    (fun (id,_) -> Flags.if_verbose msgnl (pr_id id ++ str " is defined"))
-    rfun
+    (fun ((_,id),b,_) -> 
+      if b then Flags.if_verbose msgnl (pr_id id ++ str " is redefined")
+      else Flags.if_verbose msgnl (pr_id id ++ str " is defined"))
+    tacl
 
 (***************************************************************************)
 (* Other entry points *)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 420ae8d74e..6ea0505a0b 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -63,7 +63,7 @@ val get_debug : unit -> debug_info
 
 (* Adds a definition for tactics in the table *)
 val add_tacdef :
-  bool -> (identifier Util.located * raw_tactic_expr) list -> unit
+  bool -> (identifier Util.located * bool * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
 (* Tactic extensions *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1f169394b..dbd3aacbff 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1753,7 +1753,10 @@ let abstract_args gl id =
 	  let argty = pf_type_of gl arg in
 	  let liftarg = lift (List.length ctx) arg in
 	  let liftargty = lift (List.length ctx) argty in
-	  let convertible = Reductionops.is_conv ctxenv sigma ty liftargty in
+	  let convertible = 
+	    Reductionops.is_conv ctxenv sigma
+	      (Termops.refresh_universes ty) (Termops.refresh_universes liftargty) 
+	  in
 	    match kind_of_term arg with
 	      | Var _ | Rel _ when convertible -> 
 		    (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, (Anonymous, liftarg, liftarg) :: finalargs, env)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eb62f602aa..db46c621ff 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -327,4 +327,11 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
+val make_abstract_generalize :     'a ->
+    Names.identifier ->
+    Term.constr ->
+    Sign.rel_context ->
+    Term.types ->
+    Term.types list ->
+    Term.constr list -> Term.constr list -> Term.constr -> Term.constr
 val abstract_generalize : identifier -> tactic