Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib) et suppression Stock

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

6 files changed, 74 insertions, 351 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 728430f065..1897a8ba6f 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -14,6 +14,7 @@ open Hipattern
 open Proof_trees
 open Proof_type
 open Tacmach
+open Coqlib
 
 (* This file containts the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
@@ -56,15 +57,10 @@ let h_solveRightBranch =
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let mmk         = make_module_marker [ "Logic"; "Specif" ]
-let eqpat       = put_squel mmk "eq"                 
-let sumboolpat  = put_squel mmk "sumbool"             
-let notpat      = put_squel mmk "not"   
-
 let mkDecideEqGoal rectype c1 c2 g = 
-  let equality    = mkAppA [|get_squel eqpat;rectype;c1;c2|] in
-  let disequality = mkAppA [|get_squel notpat;equality|] in
-  mkAppA [|get_squel sumboolpat;equality;disequality |]
+  let equality    = mkAppA [|build_coq_eq_data.eq (); rectype; c1; c2|] in
+  let disequality = mkAppA [|build_coq_not (); equality|] in
+  mkAppA [|build_coq_sumbool (); equality; disequality |]
 
 
 (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
@@ -101,11 +97,9 @@ let solveArg a1 a2 tac  g =
      (h_elimType decide) 
      [(eqCase tac);diseqCase;default_auto]) g
 
-let conclpatt = lazy (get_pat (put_pat mmk "{<?1>?2=?3}+{?4}"))
-
 let solveLeftBranch rectype g =
   match
-    try matches (Lazy.force conclpatt) (pf_concl g)
+    try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g)
     with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
   with 
     | _ :: lhs :: rhs :: _ -> 
@@ -118,10 +112,6 @@ let solveLeftBranch rectype g =
     | _ -> anomaly "Unexpected pattern for solveLeftBranch"
 
 
-(* The expected form of the goal for the tactic Decide Equality *)
-
-let initialpatt = lazy (get_pat (put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
-
 (* The tactic Decide Equality *)
 
 let hd_app c = match kind_of_term c with
@@ -130,7 +120,7 @@ let hd_app c = match kind_of_term c with
 
 let decideGralEquality g =
   match
-    try matches (Lazy.force initialpatt) (pf_concl g)
+    try matches (build_coq_eqdec_pattern ()) (pf_concl g)
     with Pattern.PatternMatchingFailure ->
       error "The goal does not have the expected form"
   with 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9b31819279..726131deea 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -24,6 +24,7 @@ open Tactics
 open Tacinterp
 open Tacred
 open Vernacinterp
+open Coqlib
 
 (* Rewriting tactics *)
 
@@ -44,14 +45,12 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
     | None -> error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_head hdcncl in 
+	let suffix = Declare.elimination_suffix (sort_of_goal gl) in
         let elim =
 	  if lft2rgt then
-            pf_global gl
-	      (id_of_string 
-		 (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))^"_r"))
+            pf_global gl (id_of_string (hdcncls^suffix^"_r"))
           else
-	    pf_global gl
-	      (id_of_string (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))))
+	    pf_global gl (id_of_string (hdcncls^suffix))
         in 
 	tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
    (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
@@ -176,91 +175,17 @@ let find_constructor env sigma c =
     | IsMutConstruct _ -> (hd,stack)
     | _ -> error "find_constructor"
 
-type leibniz_eq = {
-  eq   : marked_term;
-  ind  : marked_term;
-  rrec : marked_term option;
-  rect : marked_term option;
-  congr: marked_term;
-  sym  : marked_term }
-
-type sigma_type = {
-  proj1 : constr;
-  proj2 : constr;
-  elim  : constr;
-  intro : constr;
-  typ   : constr }
-
-let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ]
-
 (* Patterns *)
-let eq_pattern_mark = put_pat mmk "(eq ?1 ?2 ?3)"
-let not_pattern_mark = put_pat mmk "(not ?)"
-let imp_False_pattern_mark = put_pat mmk "? -> False"
-
-let eq_pattern () = get_pat eq_pattern_mark
-let not_pattern () = get_pat not_pattern_mark
-let imp_False_pattern () = get_pat imp_False_pattern_mark
-
-let eq = { eq = put_squel mmk "eq";
-           ind = put_squel mmk "eq_ind" ;
-           rrec = Some (put_squel mmk "eq_rec");
-           rect = Some (put_squel mmk "eq_rect");
-           congr = put_squel mmk "f_equal"  ;
-           sym  = put_squel mmk "sym_eq" }
-
-let build_eq eq = get_squel eq.eq
-let build_ind eq = get_squel eq.ind
+
+let build_coq_eq eq = eq.eq ()
+let build_ind eq = eq.ind ()
 let build_rect eq = 
   match eq.rect with
     | None -> assert false
-    | Some sq -> get_squel sq
+    | Some c -> c ()
 	  
-let eqT_pattern_mark = put_pat mmk "(eqT ?1 ?2 ?3)"
-let eqT_pattern () = get_pat eqT_pattern_mark
- 
-let eqT = { eq  = put_squel mmk "eqT";
-            ind = put_squel mmk "eqT_ind" ;
-            rrec = None;
-            rect = None;
-            congr = put_squel mmk "congr_eqT"  ;
-            sym  = put_squel mmk "sym_eqT" }
-
-let idT_pattern_mark = put_pat mmk "(identityT ?1 ?2 ?3)"
-let idT_pattern () = get_pat idT_pattern_mark
-
-let idT = { eq  = put_squel mmk "identityT";
-            ind = put_squel mmk "identityT_ind" ;
-            rrec = Some (put_squel mmk "identityT_rec")  ;
-            rect = Some (put_squel mmk "identityT_rect");
-            congr = put_squel mmk "congr_idT"  ;
-            sym  = put_squel mmk "sym_idT" }
-
 (* List of constructions depending of the initial state *)
 
-(* Initialisation part *)
-let squel_EmptyT = put_squel mmk "EmptyT"
-let squel_True   = put_squel mmk "True"
-let squel_False  = put_squel mmk "False"
-let squel_UnitT  = put_squel mmk "UnitT"
-let squel_IT     = put_squel mmk "IT"
-let squel_I      = put_squel mmk "I"
-
-(* Runtime part *)
-let build_EmptyT () = get_squel squel_EmptyT
-let build_True ()  = get_squel squel_True
-let build_False () = get_squel squel_False
-let build_UnitT () = get_squel squel_UnitT
-let build_IT ()    = get_squel squel_IT
-let build_I ()     = get_squel squel_I
-
-let pat_False_mark  = put_pat mmk "False"
-let pat_False () = get_pat pat_False_mark
-let pat_EmptyT_mark = put_pat mmk "EmptyT"
-let pat_EmptyT () = get_pat pat_EmptyT_mark
-
-let notT_pattern = put_pat mmk "(notT ?)"
-
 (* Destructuring patterns *)
 let match_eq eqn eq_pat =
   match matches eqn eq_pat with
@@ -294,14 +219,11 @@ let necessary_elimination sort_arity sort =
         [< 'sTR "no primitive equality on proofs" >]
 
 let find_eq_pattern aritysort sort = 
-  let mt =
-    match necessary_elimination aritysort sort with
-      | Set_Type       ->  eq.eq
-      | Type_Type      ->  idT.eq
-      | Set_SetorProp  ->  eq.eq
-      | Type_SetorProp ->  eqT.eq
-  in 
-  get_squel mt
+  match necessary_elimination aritysort sort with
+    | Set_Type       ->  build_coq_eq_data.eq ()
+    | Type_Type      ->  build_coq_idT_data.eq ()
+    | Set_SetorProp  ->  build_coq_eq_data.eq ()
+    | Type_SetorProp ->  build_coq_eqT_data.eq ()
 
 (* [find_positions t1 t2]
 
@@ -501,8 +423,8 @@ let construct_discriminator sigma env dirn c sort =
   let arsign,arsort = get_arity indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
-      | Type_Type -> build_UnitT (), build_EmptyT (), (Type dummy_univ)
-      | _         -> build_True (),  build_False (),  (Prop Null)
+      | Type_Type -> build_coq_UnitT (), build_coq_EmptyT (), (Type dummy_univ)
+      | _         -> build_coq_True (),  build_coq_False (),  (Prop Null)
   in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
   let cstrs = get_constructors indf in
@@ -529,22 +451,25 @@ let rec build_discriminator sigma env dirn c sort = function
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
          | Type_Type ->
-	     kont subval (build_EmptyT (),mkSort (Type(dummy_univ)))
-	 | _ -> kont subval (build_False (),mkSort (Prop Null)))
+	     kont subval (build_coq_EmptyT (),mkSort (Type(dummy_univ)))
+	 | _ -> kont subval (build_coq_False (),mkSort (Prop Null)))
 
 let find_eq_data_decompose eqn =
-  if (is_matching (eq_pattern ()) eqn) then
-    (eq, match_eq (eq_pattern ()) eqn)
-  else if (is_matching (eqT_pattern ()) eqn) then
-    (eqT, match_eq (eqT_pattern ()) eqn)
-  else if (is_matching (idT_pattern ()) eqn) then
-    (idT, match_eq (idT_pattern ()) eqn)
+  if (is_matching (build_coq_eq_pattern ()) eqn) then
+    (build_coq_eq_data, match_eq (build_coq_eq_pattern ()) eqn)
+  else if (is_matching (build_coq_eqT_pattern ()) eqn) then
+    (build_coq_eqT_data, match_eq (build_coq_eqT_pattern ()) eqn)
+  else if (is_matching (build_coq_idT_pattern ()) eqn) then
+    (build_coq_idT_data, match_eq (build_coq_idT_pattern ()) eqn)
   else
     errorlabstrm  "find_eq_data_decompose" [< >]
 
 let gen_absurdity id gl =
+(*
   if   (pf_is_matching gl (pat_False ()) (clause_type (Some id) gl)) 
     or (pf_is_matching gl (pat_EmptyT ()) (clause_type  (Some id) gl))
+*)
+  if is_empty_type (clause_type (Some id) gl)
   then
     simplest_elim (mkVar id) gl
   else
@@ -565,14 +490,14 @@ let gen_absurdity id gl =
 let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
   let env = pf_env gls in
   let (indt,_) = find_mrectype env (project gls) t in 
-  let arity = Global.mind_nf_arity indt in
+  let aritysort = mis_sort (Global.lookup_mind_specif indt) in
   let sort = pf_type_of gls (pf_concl gls) in
-  match necessary_elimination (snd (destArity arity)) (destSort sort) with
+  match necessary_elimination aritysort (destSort sort) with
     | Type_Type  ->
  	let eq_elim     = build_rect lbeq in
-	let eq_term     = build_eq lbeq in
-	let i           = build_IT () in
-	let absurd_term = build_EmptyT () in
+	let eq_term     = build_coq_eq lbeq in
+	let i           = build_coq_IT () in
+	let absurd_term = build_coq_EmptyT () in
         let h = pf_get_new_id (id_of_string "HH")gls in
         let pred= mkNamedLambda e t 
                     (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
@@ -580,8 +505,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
         in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term)
 	     
     | _ ->
-	let i           = build_I () in
-	let absurd_term = build_False ()
+	let i           = build_coq_I () in
+	let absurd_term = build_coq_False ()
 
  in
 	let eq_elim     = build_ind lbeq in
@@ -610,7 +535,6 @@ let discr id gls =
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
-	 let arity = Global.mind_nf_arity indt in
 	 let (pf, absurd_term) =
 	   discrimination_pf e (t,t1,t2) discriminator lbeq gls 
 	 in
@@ -637,9 +561,9 @@ let discrOnLastHyp gls =
 let discrClause cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
           (tclTHEN (tclTHEN hnf_in_concl intro) discrOnLastHyp) gls
-    	else if is_matching (imp_False_pattern ()) (pf_concl gls)  then
+    	else if is_matching (build_coq_imp_False_pattern ()) (pf_concl gls)then
 	  (tclTHEN intro discrOnLastHyp) gls
 	else 
 	  errorlabstrm "DiscrClause" (insatisfied_prec_message cls)
@@ -666,27 +590,6 @@ let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl
 let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
 (**)
 
-let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)"
-let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)"
-
-let constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI)
-
-let build_sigma_set () =
-  { proj1 = constant ["Specif"] "projS1";
-    proj2 = constant ["Specif"] "projS2";
-    elim = constant ["Specif"] "sigS_rec";
-    intro = constant ["Specif"] "existS";
-    typ = constant ["Specif"] "sigS" }
-
-let build_sigma_type () =
-  { proj1 = constant ["Specif"] "projT1";
-    proj2 = constant ["Specif"] "projT2";
-    elim = constant ["Specif"] "sigT_rec";
-    intro = constant ["Specif"] "existT";
-    typ = constant ["Specif"] "sigT" }
-
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
 
@@ -907,7 +810,7 @@ let inj id gls =
 	    [<'sTR "Failed to decompose the equality">];
 	tclMAP 
 	  (fun (injfun,resty) ->
-	     let pf = applist(get_squel eq.congr,
+	     let pf = applist(eq.congr (),
 			      [t;resty;injfun;
 			       try_delta_expand env sigma t1;
 			       try_delta_expand env sigma t2;
@@ -921,7 +824,7 @@ let inj id gls =
 let injClause cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
           (tclTHEN (tclTHEN hnf_in_concl intro)
              (onLastHyp (compose inj out_some))) gls
     	else
@@ -930,8 +833,6 @@ let injClause cls gls =
 	try 
 	  inj id gls
         with
-	  | Not_found ->
-	      errorlabstrm "InjClause" (not_found_message id)
           | UserError("refiner__fail",_) -> 
               errorlabstrm "InjClause" 
 		[< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >]
@@ -984,7 +885,7 @@ let decompEqThen ntac id gls =
               [<'sTR "Discriminate failed to decompose the equality">];
 	  ((tclTHEN
 	      (tclMAP (fun (injfun,resty) ->
-			 let pf = applist(get_squel lbeq.congr,
+			 let pf = applist(lbeq.congr (),
 					  [t;resty;injfun;t1;t2;
 					   mkVar id]) in
 			 let ty = pf_type_of gls pf in
@@ -999,7 +900,7 @@ let decompEq = decompEqThen (fun x -> tclIDTAC)
 let dEqThen ntac cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
 	  (tclTHEN hnf_in_concl
 	     (tclTHEN intro
          	(onLastHyp (compose (decompEqThen ntac) out_some)))) gls
@@ -1036,7 +937,7 @@ let swap_equands gls eqn =
       find_eq_data_decompose eqn
     with _ -> errorlabstrm "swap_equamds" (rewrite_msg None)
   in 
-  applist(get_squel lbeq.eq,[t;e2;e1])
+  applist(lbeq.eq (),[t;e2;e1])
 
 let swapEquandsInConcl gls =
   let (lbeq,(t,e1,e2)) =
@@ -1044,7 +945,7 @@ let swapEquandsInConcl gls =
       find_eq_data_decompose (pf_concl gls)
     with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) 
   in
-  let sym_equal = get_squel lbeq.sym in
+  let sym_equal = lbeq.sym () in
   refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls
 
 let swapEquandsInHyp id gls =
@@ -1059,15 +960,15 @@ let swapEquandsInHyp id gls =
 
 let find_elim  sort_of_gl  lbeq =
   match kind_of_term sort_of_gl  with
-    | IsSort(Prop Null)  (* Prop *)  ->  (get_squel lbeq.ind, false)  
+    | IsSort(Prop Null)  (* Prop *)  ->  (lbeq.ind (), false)  
     | IsSort(Prop Pos)   (* Set *)   ->  
 	(match lbeq.rrec with
-           | Some eq_rec -> (get_squel eq_rec, false) 
+           | Some eq_rec -> (eq_rec (), false) 
 	   | None -> errorlabstrm "find_elim"
 		 [< 'sTR "this type of elimination is not allowed">])
     | _ (* Type *) -> 
         (match lbeq.rect with
-           | Some eq_rect -> (get_squel eq_rect, true) 
+           | Some eq_rect -> (eq_rect (), true) 
            | None -> errorlabstrm "find_elim"
 		 [< 'sTR "this type of elimination is not allowed">])
 
@@ -1078,7 +979,7 @@ let find_elim  sort_of_gl  lbeq =
 let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls =
   let e = pf_get_new_id  (id_of_string "e") gls in 
   let h = pf_get_new_id  (id_of_string "HH") gls in 
-  let eq_term = get_squel lbeq.eq in
+  let eq_term = lbeq.eq () in
   (mkNamedLambda e t 
      (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
         (lift 1 body))) 
@@ -1135,18 +1036,18 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
  *)
 
 let match_sigma ex ex_pat =
-  match matches (get_pat ex_pat) ex with
+  match matches ex_pat ex with
     | [(1,a);(2,p);(3,car);(4,cdr)] -> (a,p,car,cdr)
     | _ ->
 	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
 
 let find_sigma_data_decompose ex =
   try
-    let subst = match_sigma ex existS_pattern in
+    let subst = match_sigma ex (build_coq_existS_pattern ()) in
     (build_sigma_set (),subst)
   with PatternMatchingFailure ->
     (try 
-       let subst = match_sigma ex existT_pattern in
+       let subst = match_sigma ex (build_coq_existT_pattern ()) in
        (build_sigma_type (),subst)
      with PatternMatchingFailure -> 
        errorlabstrm "find_sigma_data_decompose" [< >])
@@ -1352,7 +1253,7 @@ let sub_term_with_unif cref ceq =
 let general_rewrite_in lft2rgt id (c,lb) gls =
   let typ_id =
     (try
-       let (_,ty) = lookup_named id (pf_env gls) in (body_of_type ty)
+       let (_,ty) = lookup_named id (pf_env gls) in ty
      with Not_found -> 
        errorlabstrm "general_rewrite_in" 
 	 [< 'sTR"No such hypothesis : "; pr_id id >])
@@ -1375,10 +1276,10 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
            | None ->
                errorlabstrm "general_rewrite_in" 
 		 [<'sTR "Nothing to rewrite in: "; pr_id id>]
-           |Some (l2,nb_occ) ->
-               (tclTHENSI 
-		  (tclTHEN 
-		     (tclTHEN (generalize [(pf_global gls id)]) 
+           | Some (l2,nb_occ) ->
+               (tclTHENSI
+		  (tclTHEN
+		     (tclTHEN (generalize [(pf_global gls id)])
 			(reduce (Pattern [(list_int nb_occ 1 [],l2,
 					   pf_type_of gls l2)]) []))
 		     (general_rewrite_bindings lft2rgt (c,lb))) 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ba59183cb3..ba519cb2f2 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -10,70 +10,9 @@ open Inductive
 open Evd
 open Environ
 open Proof_trees
-open Stock
 open Clenv
 open Pattern
-
-(* The pattern table for tactics. *)
-
-(* Description: see the interface. *)
-
-(* First part : introduction of term patterns *)
-
-type module_mark = Stock.module_mark
-
-let parse_astconstr s =
-  try 
-    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
-  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
-    error "Syntax error : not a construction" 
-
-(* Patterns *)
-let parse_pattern s =
-  Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
-
-type marked_pattern = (int list * constr_pattern) Stock.stocked
-
-let (pattern_stock : (int list * constr_pattern) Stock.stock) =
-  Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
-
-let put_pat = Stock.stock pattern_stock
-let get_pat tm = snd (Stock.retrieve pattern_stock tm)
-
-let make_module_marker = Stock.make_module_marker
-
-(* Squeletons *)
-let parse_squeleton s =
-  let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_astconstr s) in
-  (collect_metas c, c)
-
-type marked_term = (int list * constr) Stock.stocked
-
-let (squeleton_stock : (int list * constr) Stock.stock) =
-  Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton }
-
-let put_squel = Stock.stock squeleton_stock
-let get_squel_core = Stock.retrieve squeleton_stock
-
-(* Sera mieux avec des noms qualifiés *)
-let get_reference mods s =
-  if list_subset mods (Library.loaded_modules()) then
-    try Declare.global_reference CCI (id_of_string s)
-    with Not_found ->
-      error ("get_reference: "^s^"is not defined in the given modules")
-  else error "The required modules are not open"
-
-let soinstance squel arglist =
-  let mvs,c = get_squel_core squel in
-  let mvb = List.combine mvs arglist in 
-  Reduction.local_strong (Reduction.whd_meta mvb) c
-
-let get_squel m =
-  let mvs, c = get_squel_core m in
-  if mvs = [] then c
-  else errorlabstrm "get_squel"
-    [< Printer.prterm c;
-       'sPC; 'sTR "is not a closed squeleton, use 'soinstance'" >]
+open Coqlib
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -85,8 +24,6 @@ let get_squel m =
   
   -- Eduardo (6/8/97). *)
 
-let mmk = make_module_marker ["Prelude"]
-
 type 'a matching_function = constr -> 'a option
 
 type testing_function  = constr -> bool
@@ -177,9 +114,6 @@ let is_unit_type t = op2bool (match_with_unit_type t)
    inductive binary relation R, so that R has only one constructor
    stablishing its reflexivity.  *)
 
-let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)"
-let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)"
-
 let match_with_equation  t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
@@ -187,8 +121,8 @@ let match_with_equation  t =
         let constr_types = Global.mind_nf_lc ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
-           (is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
-            is_matching (get_pat refl_rel_pat2) constr_types.(0)) 
+           (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) ||
+            is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0)) 
         then 
 	  Some (hdapp,args)
         else 
@@ -197,11 +131,9 @@ let match_with_equation  t =
 
 let is_equation t = op2bool (match_with_equation  t)
 
-let arrow_pat = put_pat mmk "(?1 -> ?2)"
-
 let match_with_nottype t =
   try
-    match matches (get_pat arrow_pat) t with
+    match matches (build_coq_arrow_pattern ()) t with
       |	[(1,arg);(2,mind)] ->
 	  if is_empty_type mind then Some (mind,arg) else None
       | _ -> anomaly "Incorrect pattern matching" 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 16be20610a..306a740439 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -11,72 +11,8 @@ open Pattern
 open Proof_trees
 (*i*)
 
-(* The pattern table for tactics. *)
-
-(* The idea is that we want to write tactic files which are only
-   "activated" when certain modules are loaded and imported.  Already,
-   the question of how to store the tactics is hard, and we will not
-   address that here.  However, the question arises of how to store
-   the patterns that we will want to use for term-destructuring, and
-   the solution proposed is that we will store patterns with a
-   "module-marker", telling us which modules have to be open in order
-   to use the pattern.  So we will write:
-   \begin{verbatim}
-   let mark = make_module_marker ["<module-name>";<module-name>;...];;
-   let p1 = put_pat mark "<parseable pattern goes here>";;
-   \end{verbatim}
-   And now, we can use [(get p1)]
-   to get the term which corresponds to this pattern, already parsed
-   and with the global names adjusted.
-
-   In other words, we will have the term which we would have had if we
-   had done an:
-   \begin{verbatim}
-        constr_of_com mt_ctxt (initial_sign()) "<text here>"
-   \end{verbatim}
-   except that it will be computed at module-opening time, rather than
-   at tactic-application time.  The ONLY difference will be that
-   no implicit syntax resolution will happen. *)
-
-(* A pattern is intented to be pattern-matched (using functions
-   [somatch] and co), while a squeleton is a term with holes intented to
-   be substituted by [soinstance] *)
-
-(*s First part : introduction of term patterns and term squeletons *)
-
-(* [make_module_marker modl] makes a key from the list of
-   vernacular modules [modl] where names in a pattern or squeleton has
-   to be searched *)
-
-type module_mark = Stock.module_mark
-val make_module_marker : string list -> module_mark
-
-(* [put_pat mmk s] declares a pattern [s] to be parsed using the
-   definitions in the modules associated to the key [mmk] *)
-
-type marked_pattern
-val put_pat            : module_mark -> string -> marked_pattern
-val get_pat            : marked_pattern -> constr_pattern
-
-(* [put_squel mmk s] declares an open term [s] to be parsed using the
-   definitions in the modules associated to the key [mmk] *)
-
-type marked_term
-val put_squel          : module_mark -> string -> marked_term
-
-(*i val get_squel          : marked_term -> constr i*)
-
-(*i Remplacé par Astterm.interp_constrpattern
-val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
-i*)
-
-(* [get_reference mods id] interprets [id] as a global identifier
-   assuming defined in the modules listed in [mods] *)
-
-val get_reference : string list -> string -> constr
-
-(*s Second part : Given a term with second-order variables in it,
-   represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
+(*s Given a term with second-order variables in it,
+   represented by Meta's, and possibly applied using SoApp
    terms, this function will perform second-order, binding-preserving,
    matching, in the case where the pattern is a pattern in the sense
    of Dale Miller.
@@ -92,38 +28,7 @@ val get_reference : string list -> string -> constr
 
    When we reach a second-order application, we ask that the
    intersection of the free-rels of the term and the current stack be
-   contained in the arguments of the application, and in that case, we
-   construct a [DLAM] with the names on the stack. *)
-
-
-(* [dest_somatch c pat] matches [c] against [pat] and returns the resulting
-   assignment of metavariables; it raises [PatternMatchingFailure] if
-   not matchable *)
-(*i
-val dest_somatch : constr -> marked_pattern -> constr list
-
-(* [somatches c pat] just tells if [c] matches against [pat] *)
-
-val somatches    : constr -> marked_pattern -> bool
-
-(* [dest_somatch_conv env sigma] matches up to conversion in
-   environment [(env,sgima)] when constants in pattern are concerned;
-   it raises [PatternMatchingFailure] if not matchable *)
-
-val dest_somatch_conv :
-  Environ.env -> 'a evar_map -> constr -> marked_pattern -> (int * constr) list
-
-(* [somatches_conv env sigma c pat] tells if [c] matches against [pat]
-   up to conversion for constants in patterns *)
-
-val somatches_conv :
-  Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
-i*)
-
-val soinstance   : marked_term -> constr list -> constr 
-
-(* This works only for squeleton without metavariables *)
-val get_squel    : marked_term -> constr 
+   contained in the arguments of the application *)
 
 val is_imp_term : constr -> bool
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index da43bd0eb2..9b81e87e6a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -52,13 +52,13 @@ open Pattern
 
 let dest_match_eq gls eqn =
   try 
-    pf_matches gls (eq_pattern ()) eqn
+    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
   with PatternMatchingFailure -> 
     (try 
-       pf_matches gls (eqT_pattern ()) eqn
+       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
      with PatternMatchingFailure -> 
        (try 
-	  pf_matches gls (idT_pattern ()) eqn
+	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
         with PatternMatchingFailure ->
 	  errorlabstrm "dest_match_eq" 
 	    [< 'sTR "no primitive equality here" >]))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f532166d05..08e35f50e2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -21,6 +21,7 @@ open Logic
 open Clenv
 open Tacticals
 open Hipattern
+open Coqlib
 
 exception Bound
 
@@ -58,6 +59,7 @@ let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match kind_of_term t with
     | IsProd (_,_,c2)  -> head_constr_bound c2 l 
+    | IsLetIn (_,_,_,c2) -> head_constr_bound c2 l 
     | IsApp (f,args)  -> 
 	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
     | IsConst _        -> t::l
@@ -1558,19 +1560,12 @@ let contradiction_on_hyp id gl =
   else 
     error "Not a contradiction"
 
-let constant dir s = 
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI)
-
-let coq_False = lazy (constant ["Logic"] "False")
-let coq_not = lazy (constant ["Logic"] "not")
-
 (* Absurd *)
 let absurd c gls =
   (tclTHENS
-     (tclTHEN (elim_type (Lazy.force coq_False)) (cut c)) 
+     (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
      ([(tclTHENS
-          (cut (applist(Lazy.force coq_not,[c]))) 
+          (cut (applist(build_coq_not (),[c]))) 
 	  ([(tclTHEN intros
 	       ((fun gl ->
 		   let ida = pf_nth_hyp_id gl 1
@@ -1585,7 +1580,7 @@ let dyn_absurd = function
   | l             -> bad_tactic_args "absurd" l
 
 let contradiction gls = 
-  tclTHENLIST [ intros; elim_type (Lazy.force coq_False); assumption ] gls
+  tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls
 
 let dyn_contradiction = function
   | []  -> contradiction