modules Indrec, Tacentries, Hiddentac

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

5 files changed, 165 insertions, 2 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
new file mode 100644
index 0000000000..07ef757a56
--- /dev/null
+++ b/tactics/hiddentac.ml
@@ -0,0 +1,40 @@
+
+(* $Id$ *)
+
+open Term
+open Proof_trees
+open Tacmach
+open Tacentries
+
+(* These tactics go through the interpreter. They left a trace in the proof
+   tree when they are called. *)
+
+let h_clear ids         = v_clear  [(Clause ids)]
+let h_move dep id1 id2  = 
+ (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
+let h_contradiction     = v_contradiction []
+let h_reflexivity       = v_reflexivity   []
+let h_symmetry          = v_symmetry      []
+let h_assumption        = v_assumption    []
+let h_absurd c          = v_absurd [(Constr c)]
+let h_exact  c          = v_exact  [(Constr c)]
+let h_one_constructor i = v_constructor [(Integer i)]
+let h_any_constructor   = v_constructor []
+let h_transitivity c    = v_transitivity [(Constr c)]
+let h_simplest_left     = v_left [(Cbindings [])]
+let h_simplest_right    = v_right [(Cbindings [])]
+let h_split     c       = v_split [(Constr c);(Cbindings [])]
+let h_apply c s         = v_apply  [(Constr c);(Cbindings s)]
+let h_simplest_apply c  = v_apply  [(Constr c);(Cbindings [])]
+let h_cut      c        = v_cut [(Constr c)]
+let h_simplest_elim c   = v_elim [(Constr c);(Cbindings [])]
+let h_elimType     c    = v_elimType [(Constr c)]
+let h_inductionInt  i   = v_induction[(Integer i)]
+let h_inductionId   id  = v_induction[(Identifier id)]
+let h_simplest_case   c = v_case [(Constr c);(Cbindings [])]
+let h_caseType        c = v_caseType [(Constr c)]
+let h_destructInt  i    = v_destruct [(Integer i)]
+let h_destructId   id   = v_destruct [(Identifier id)]
+
+
+
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
new file mode 100644
index 0000000000..1d9b25757a
--- /dev/null
+++ b/tactics/hiddentac.mli
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Proof_trees
+open Tacmach
+open Tacentries
+(*i*)
+
+val h_clear           : identifier list -> tactic
+val h_move            : bool -> identifier -> identifier -> tactic
+val h_contradiction   : tactic
+val h_reflexivity     : tactic
+val h_symmetry        : tactic
+val h_assumption      : tactic
+val h_absurd          : constr -> tactic
+val h_exact           : constr -> tactic
+val h_one_constructor : int -> tactic
+val h_any_constructor : tactic
+val h_transitivity    : constr -> tactic
+val h_simplest_left   : tactic
+val h_simplest_right  : tactic
+val h_split           : constr -> tactic
+val h_apply           : constr -> constr substitution -> tactic
+val h_simplest_apply  : constr -> tactic 
+val h_cut             : constr -> tactic 
+val h_simplest_elim   : constr -> tactic
+val h_elimType        : constr -> tactic
+val h_simplest_case   : constr -> tactic
+val h_caseType        : constr -> tactic
+val h_inductionInt    : int -> tactic 
+val h_inductionId     : identifier -> tactic 
+val h_destructInt     : int -> tactic
+val h_destructId      : identifier -> tactic
+
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
new file mode 100644
index 0000000000..a91c5f4fc2
--- /dev/null
+++ b/tactics/tacentries.ml
@@ -0,0 +1,45 @@
+
+(* $Id$ *)
+
+open Proof_trees
+open Tacmach
+open Tactics
+open Tacticals
+
+let v_absurd        = hide_tactic "Absurd"        dyn_absurd
+let v_contradiction = hide_tactic "Contradiction" dyn_contradiction
+let v_reflexivity   = hide_tactic "Reflexivity"   dyn_reflexivity
+let v_symmetry      = hide_tactic "Symmetry"      dyn_symmetry
+let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
+let v_intro         = hide_tactic "Intro"         dyn_intro
+let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
+let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
+let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
+let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL
+let v_assumption    = hide_tactic "Assumption"    dyn_assumption
+let v_exact         = hide_tactic "Exact"         dyn_exact
+let v_reduce        = hide_tactic "Reduce"        dyn_reduce
+let v_change        = hide_tactic "Change"        dyn_change
+let v_constructor   = hide_tactic "Constructor"   dyn_constructor
+let v_left          = hide_tactic "Left"          dyn_left
+let v_right         = hide_tactic "Right"         dyn_right
+let v_split         = hide_tactic "Split"         dyn_split
+let v_clear         = hide_tactic "Clear"         dyn_clear
+let v_move          = hide_tactic "Move"          dyn_move
+let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
+let v_apply         = hide_tactic "Apply"         dyn_apply
+let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
+let v_cut           = hide_tactic "Cut"           dyn_cut
+let v_lettac        = hide_tactic "LetTac"        dyn_lettac
+let v_generalize    = hide_tactic "Generalize"    dyn_generalize
+let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
+let v_specialize    = hide_tactic "Specialize"    dyn_new_hyp
+let v_elim          = hide_tactic "Elim"          dyn_elim
+let v_elimType      = hide_tactic "ElimType"      dyn_elim_type
+let v_induction     = hide_tactic "Induction"     dyn_induct
+let v_case          = hide_tactic "Case"          dyn_case
+let v_caseType      = hide_tactic "CaseType"      dyn_case_type
+let v_destruct      = hide_tactic "Destruct"      dyn_destruct
+let v_fix           = hide_tactic "Fix"           dyn_mutual_fix
+let v_cofix         = hide_tactic "Cofix"         dyn_mutual_cofix
+
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
new file mode 100644
index 0000000000..ed19fd8d82
--- /dev/null
+++ b/tactics/tacentries.mli
@@ -0,0 +1,41 @@
+
+(* $Id$ *)
+
+(*i*)
+open Proof_trees
+open Tacmach
+(*i*)
+
+val v_absurd        : tactic_arg list -> tactic
+val v_contradiction : tactic_arg list -> tactic
+val v_reflexivity   : tactic_arg list -> tactic
+val v_symmetry      : tactic_arg list -> tactic
+val v_transitivity  : tactic_arg list -> tactic
+val v_intro         : tactic_arg list -> tactic
+val v_introsUntil   : tactic_arg list -> tactic
+val v_tclIDTAC      : tactic_arg list -> tactic
+val v_assumption    : tactic_arg list -> tactic
+val v_exact         : tactic_arg list -> tactic
+val v_reduce        : tactic_arg list -> tactic
+val v_constructor   : tactic_arg list -> tactic
+val v_left          : tactic_arg list -> tactic
+val v_right         : tactic_arg list -> tactic
+val v_split         : tactic_arg list -> tactic
+val v_clear         : tactic_arg list -> tactic
+val v_move          : tactic_arg list -> tactic
+val v_move_dep      : tactic_arg list -> tactic
+val v_apply         : tactic_arg list -> tactic
+val v_cutAndResolve : tactic_arg list -> tactic
+val v_cut           : tactic_arg list -> tactic
+val v_lettac        : tactic_arg list -> tactic
+val v_generalize    : tactic_arg list -> tactic
+val v_generalize_dep : tactic_arg list -> tactic
+val v_specialize    : tactic_arg list -> tactic
+val v_elim          : tactic_arg list -> tactic
+val v_elimType      : tactic_arg list -> tactic
+val v_induction     : tactic_arg list -> tactic
+val v_case          : tactic_arg list -> tactic
+val v_caseType      : tactic_arg list -> tactic
+val v_destruct      : tactic_arg list -> tactic
+val v_fix           : tactic_arg list -> tactic
+val v_cofix         : tactic_arg list -> tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 49c384df4a..bd66561dd8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -374,7 +374,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
   let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
-  let elim  = Indrec.make_case_gen sigma ity sort in  
+  let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -383,7 +383,7 @@ let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
-  let elim  = Indrec.make_case_nodep sigma ity sort in  
+  let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl