From bfc03c53882d7334e4fb327362c354397a8462ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Oct 2008 19:22:27 +0000
Subject: Fixes and refinements regarding occurrence selection: - make the
 modifiers "value of" and "type of" for "set" working (it was not!), - clear
 unselected hypotheses in the "in" clause of "induction/destruct" when   the
 destructed term is a variable (experimental), - support for generalization of
 hypotheses in the induction hypotheses using   the "in" clause of "induction"
 (e.g. "induction n in m, H" will   generalize over m -- would it be better to
 have an explicit   "over"/"generalizing" clause ?). Added clause "as" to
 "apply in".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/firstorder/rules.ml                    | 2 +-
 contrib/funind/functional_principles_proofs.ml | 2 +-
 contrib/funind/recdef.ml                       | 2 +-
 contrib/interface/xlate.ml                     | 1 +
 contrib/setoid_ring/newring.ml4                | 1 +
 5 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'contrib')

diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index 813e951cf8..6c00e4eace 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -213,4 +213,4 @@ let normalize_evaluables=
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some ((_,id),_)-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly))
+	   ((Rawterm.all_occurrences_expr,id),InHypTypeOnly))
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 971dada68f..6241eb1de4 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1347,7 +1347,7 @@ let build_clause eqs =
   {
     Tacexpr.onhyps = 
       Some (List.map 
-	      (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
+	      (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
 	      eqs
 	   );
     Tacexpr.concl_occs = Rawterm.no_occurrences_expr 
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 8161e890dc..528c276c05 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -1160,7 +1160,7 @@ let rec introduce_all_values_eq cont_tac functional termine
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
                              (global_of_constr functional))]
-             ((all_occurrences_expr, heq2), Tacexpr.InHyp);
+             ((all_occurrences_expr, heq2), InHyp);
            tclTHENS
 	     (fun gls -> 
 		let t_eq = compute_renamed_type gls (mkVar heq2) in 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7b654b74b7..26b9be8707 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -7,6 +7,7 @@ open Names;;
 open Ascent;;
 open Genarg;;
 open Rawterm;;
+open Termops;;
 open Tacexpr;;
 open Vernacexpr;;
 open Decl_kinds;;
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c3bc458e2d..fc66b1c971 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -19,6 +19,7 @@ open Environ
 open Libnames
 open Tactics
 open Rawterm
+open Termops
 open Tacticals
 open Tacexpr
 open Pcoq
-- 
cgit v1.2.3