Add the ability to specify what to do with free variables in instance

declarations. By default, print the list of implicitely generalized
variables. Implement new commands Add Parametric Relation/Morphism for...
parametric relations and morphisms. Now the Add * commands are strict
about free vars and will fail if there remain some. Parametric just allows to
give a variable context. Also, correct a bug in generalization of
implicits that ordered the variables in the wrong order.


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

1 files changed, 159 insertions, 97 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f00515ab6..9b0bb188b 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -550,8 +550,8 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
 	    new_evar isevars env relty
       | Some x -> f x
   in
-  let rec aux t l =
-    let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) t in
+  let rec aux ty l =
+    let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
     match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
 	  let (b, arg, evars) = aux b cstrs in
@@ -563,7 +563,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota t in
+		let t = Reductionops.nf_betaiota ty in
 		let rel = mk_relty t None in 
 		  t, rel, [t, rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
@@ -680,7 +680,7 @@ let rewrite2_unif_flags = {
 (* let unification_rewrite c1 c2 cl but gl =  *)
 (*   let (env',c1) = *)
 (*     try *)
-(*       (\* ~flags:(false,true) to allow to mark occurences that must not be *)
+(*       (\* ~flags:(false,true) to allow to mark occurrences that must not be *)
 (*          rewritten simply by replacing them with let-defined definitions *)
 (*          in the context *\) *)
 (*       w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *)
@@ -989,10 +989,10 @@ open Genarg
 open Extraargs
 
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ]
+| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None ]
 | [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ]
 END
 
@@ -1084,25 +1084,31 @@ TACTIC EXTEND setoid_rewrite
    -> [ cl_rewrite_clause c o [] None ]
  | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] ->
       [ cl_rewrite_clause c o [] (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) ] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o occ None]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id)] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] ->
       [ cl_rewrite_clause c o occ (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ)] ->
+ | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] ->
       [ cl_rewrite_clause c o occ (Some (([],id), []))]
 END
 
 (* let solve_obligation lemma =  *)
 (*   tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *)
 (*     (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *)
-    
+
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
 
-let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit,
-				 CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
-					  [a;aeq]))
+let declare_an_instance n s args =
+  ((dummy_loc,Name n), Explicit,
+  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
+	   args))
 
-let anew_instance instance fields = new_instance [] instance fields None
+let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
+
+let anew_instance binders instance fields = 
+  new_instance binders instance fields 
+    ~on_free_vars:Classes.fail_on_free_vars
+    None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1111,75 +1117,85 @@ let require_library dirpath =
 let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
-  if not (Library.library_is_opened dir) || not (Library.library_is_loaded dir) then
+  if (* not (Library.library_is_opened dir) ||  *)not (Library.library_is_loaded dir) then
     error ("Library "^(list_last d)^" has to be required first")
 
 let init_setoid () =
   check_required_library ["Coq";"Setoids";"Setoid"]
 
-let declare_instance_refl a aeq n lemma = 
+let declare_instance_refl binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" 
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
 
-let declare_instance_sym a aeq n lemma = 
+let declare_instance_sym binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric"
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "symmetry"),[],lemma)]
 
-let declare_instance_trans a aeq n lemma = 
+let declare_instance_trans binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" 
-  in anew_instance instance 
+  in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
 
-let declare_relation a aeq n refl symm trans = 
+let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
   match (refl,symm,trans) with 
       (None, None, None) -> 
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" 
-	in ignore(anew_instance instance [])
+	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation"
+	in ignore(anew_instance binders instance [])
     | (Some lemma1, None, None) -> 
-	ignore (declare_instance_refl a aeq n lemma1)
+	ignore (declare_instance_refl binders a aeq n lemma1)
     | (None, Some lemma2, None) -> 
-	ignore (declare_instance_sym a aeq n lemma2)
+	ignore (declare_instance_sym binders a aeq n lemma2)
     | (None, None, Some lemma3) -> 
-	ignore (declare_instance_trans a aeq n lemma3)
+	ignore (declare_instance_trans binders a aeq n lemma3)
     | (Some lemma1, Some lemma2, None) -> 
-	ignore (declare_instance_refl a aeq n lemma1); 
-	ignore (declare_instance_sym a aeq n lemma2)
+	ignore (declare_instance_refl binders a aeq n lemma1); 
+	ignore (declare_instance_sym binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl a aeq n lemma1 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
-	    anew_instance instance 
+	    anew_instance binders instance 
 	      [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl);
 	       ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)])
     | (None, Some lemma2, Some lemma3) -> 
-	let lemma_sym = declare_instance_sym a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
-	    anew_instance instance 
+	    anew_instance binders instance 
 	      [((dummy_loc,id_of_string "per_sym"),  [], mkIdentC lemma_sym);
 	       ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)])
      | (Some lemma1, Some lemma2, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl a aeq n lemma1 in 
-	let lemma_sym = declare_instance_sym a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
+	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
-	    anew_instance instance 
-	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+	  anew_instance binders instance 
+	    [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+	     ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+	     ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+
+type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+
+let (wit_binders_let : Genarg.tlevel binders_let_argtype),
+  (globwit_binders_let : Genarg.glevel binders_let_argtype),
+  (rawwit_binders_let : Genarg.rlevel binders_let_argtype) =
+  Genarg.create_arg "binders_let"
+
+open Pcoq.Constr
 
 VERNAC COMMAND EXTEND AddRelation
-    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
+
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)  
 	"as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) None None ]
@@ -1208,6 +1224,40 @@ VERNAC COMMAND EXTEND AddRelation3
       [ declare_relation a aeq n None None (Some lemma3) ] 
 END
 
+VERNAC COMMAND EXTEND AddParametricRelation
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+	"reflexivity" "proved" "by" constr(lemma1) 
+	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+	"reflexivity" "proved" "by" constr(lemma1)  
+	"as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)  "as" ident(n) ] -> 
+      [ declare_relation ~binders:b a aeq n None None None ]
+END
+
+VERNAC COMMAND EXTEND AddParametricRelation2
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) 
+      "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
+END
+
+VERNAC COMMAND EXTEND AddParametricRelation3
+    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) 
+      "as" ident(n) ] ->
+      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] 
+  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+	"as" ident(n) ] ->  
+      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] 
+END
+
 let mk_qualid s =
   Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s)
 
@@ -1271,10 +1321,10 @@ let build_morphism_signature m =
     in aux t
   in
   let t', sig_, evars = build_signature isevars env t cstrs None snd in
-  let _ = List.iter 
+  let _ = List.iter
     (fun (ty, rel) -> 
       let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
-	ignore(Evarutil.e_new_evar isevars env default))
+	ignore (Evarutil.e_new_evar isevars env default))
     evars
   in
   let morph = 
@@ -1283,7 +1333,7 @@ let build_morphism_signature m =
   let evd = resolve_all_evars_once false (true, 15) env
     (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in
     Evarutil.nf_isevar evd morph
-
+	
 let default_morphism sign m =
   let env = Global.env () in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -1297,55 +1347,67 @@ let default_morphism sign m =
   let mor = resolve_one_typeclass env morph in
     mor, respect_projection mor morph
     	  
+let add_setoid binders a aeq t n =
+  init_setoid ();
+  let lemma_refl = declare_instance_refl binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
+  let lemma_sym = declare_instance_sym binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let lemma_trans = declare_instance_trans binders a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
+  let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
+  in ignore(
+    anew_instance binders instance
+      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+
+let add_morphism_infer m n =
+  init_setoid ();
+  let instance_id = add_suffix n "_Morphism" in
+  let instance = build_morphism_signature m in
+    if Lib.is_modtype () then 
+      let cst = Declare.declare_internal_constant instance_id
+	(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+      in
+	add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+	declare_projection n instance_id (ConstRef cst)
+    else
+      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	Flags.silently 
+	  (fun () ->
+	    Command.start_proof instance_id kind instance 
+	      (fun _ -> function
+		  Libnames.ConstRef cst -> 
+		    add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+		    declare_projection n instance_id (ConstRef cst)
+		| _ -> assert false);
+	    Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
+	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () 
+
+let add_morphism binders m s n =
+  init_setoid ();
+  let instance_id = add_suffix n "_Morphism" in
+  let instance = 
+    ((dummy_loc,Name instance_id), Explicit,
+    CAppExpl (dummy_loc, 
+	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
+	     [cHole; s; m]))
+  in	  
+  let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
+    ignore(new_instance binders instance []
+	      ~on_free_vars:Classes.fail_on_free_vars
+	      ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+	      None)
+
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [	init_setoid ();
-	let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
-	let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-	let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
-	in ignore(
-	    anew_instance instance
-	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])]
+     [ add_setoid [] a aeq t n ]
+  | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     [	add_setoid binders a aeq t n ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ init_setoid ();
-	let instance_id = add_suffix n "_Morphism" in
-	let instance = build_morphism_signature m in
-	  if Lib.is_modtype () then 
-	    let cst = Declare.declare_internal_constant instance_id
-	      (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	    in
-	      add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
-	      declare_projection n instance_id (ConstRef cst)
-	  else
-	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	      Flags.silently 
-		(fun () ->
-		  Command.start_proof instance_id kind instance 
-		    (fun _ -> function
-			Libnames.ConstRef cst -> 
-			  add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
-			  declare_projection n instance_id (ConstRef cst)
-		      | _ -> assert false);
-		  Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
-	      Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () ]
-
+      [ add_morphism_infer m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ init_setoid ();
-	let instance_id = add_suffix n "_Morphism" in
-	let instance = 
-	  ((dummy_loc,Name instance_id), Explicit,
-	  CAppExpl (dummy_loc, 
-		   (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
-		   [cHole; s; m]))
-	in	  
-	let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-	  ignore(new_instance [] instance []
-		    ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
-		    None)
-      ]
+      [ add_morphism [] m s n ]
+  | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
+      [ add_morphism binders m s n ]
 END
 
 (** Bind to "rewrite" too *)
@@ -1375,7 +1437,7 @@ let check_evar_map_of_evars_defs evd =
 let unification_rewrite l2r c1 c2 cl rel but gl = 
   let (env',c') =
     try
-      (* ~flags:(false,true) to allow to mark occurences that must not be
+      (* ~flags:(false,true) to allow to mark occurrences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
       Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
@@ -1408,15 +1470,15 @@ let get_hyp gl c clause l2r =
 	
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
-let general_s_rewrite l2r c ~new_goals gl =
+let general_s_rewrite l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo = ref (get_hyp gl c None l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] None gl
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs None gl
 
-let general_s_rewrite_in id l2r c ~new_goals gl =
+let general_s_rewrite_in id l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo = ref (get_hyp gl c (Some id) l2r) in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] (Some (([],id), [])) gl
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs (Some (([],id), [])) gl
 
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])