Fix splitting evars tactics and stop dropping evar constraints when

building a new goal evar defs.
Allow customization of the reduction function applied to subtac
obligations.


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

3 files changed, 21 insertions, 17 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index a10ef1cb66..f1bdd64092 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -149,7 +149,7 @@ let move_after (id, ev, deps as obl) l =
 	  if Intset.is_empty restdeps' then
 	    obl' :: obl :: tl
 	  else obl' :: aux restdeps' tl
-    | [] -> assert false
+    | [] -> [obl]
   in aux (Intset.remove id deps) l
     
 let sort_dependencies evl =
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 9619aa4226..e0ba212c53 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -21,8 +21,8 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
-let reduce =
-  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+let reduce c =
+  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty c
 
 exception NoObligations of identifier option
 
@@ -61,6 +61,7 @@ type program_info = {
   prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
+  prg_reduce : constr -> constr;
   prg_hook : Tacexpr.declaration_hook;
 }
 
@@ -248,7 +249,7 @@ let declare_mutual_definition l =
 	let subs, typ = (subst_body true x) in
 	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
 	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
-	  reduce term, reduce typ, x.prg_implicits) l)
+	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixkind = Option.get first.prg_fixkind in
@@ -278,8 +279,8 @@ let declare_mutual_definition l =
       List.iter progmap_remove l; kn
       
 let declare_obligation prg obl body =
-  let body = reduce body in
-  let ty = reduce obl.obl_type in
+  let body = prg.prg_reduce body in
+  let ty = prg.prg_reduce obl.obl_type in
   match obl.obl_status with
   | Expand -> { obl with obl_body = Some body }
   | Define opaque ->
@@ -299,9 +300,7 @@ let declare_obligation prg obl body =
 	print_message (Subtac_utils.definition_message obl.obl_name);
 	{ obl with obl_body = Some (mkConst constant) }
 
-let red = Reductionops.nf_betaiota Evd.empty
-
-let init_prog_info n b t deps fixkind notations obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -315,13 +314,13 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = red t; obl_status = o;
+	      obl_location = l; obl_type = reduce t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
-    { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
+    { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
-      prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; }
 
 let get_prog name =
   let prg_infos = !from_prg in
@@ -557,9 +556,10 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n term t [] None [] obls implicits kind hook in
+  let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Flags.if_verbose ppnl (str ".");
@@ -574,12 +574,14 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) 
+    ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in
-	  ProgMap.add n prg acc)
+	let prg = init_prog_info n (Some b) t deps (Some fixkind) 
+	  notations obls imps kind reduce hook 
+	in ProgMap.add n prg acc)
       !from_prg l
   in
     from_prg := upd;
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index c1e8d31c0e..aed5b58b7a 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -27,6 +27,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
   ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
+  ?reduce:(Term.constr -> Term.constr) ->
   ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -40,6 +41,7 @@ val add_mutual_definitions :
       (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
+  ?reduce:(Term.constr -> Term.constr) ->
   ?hook:Tacexpr.declaration_hook ->
   notations ->
   fixpoint_kind -> unit