From 3c22073b7a03391cb8a88bf5ec6cfb0f4ba2318d Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 23 Nov 2000 07:55:58 +0000
Subject: Reparation IsMutConstruct + Transparent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml            |  2 +-
 proofs/clenv.ml           |  2 +-
 tactics/eauto.ml          | 13 +++++++------
 toplevel/vernacentries.ml |  3 ++-
 4 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/kernel/term.ml b/kernel/term.ml
index 1751c5d82d..e29a9edcd0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -479,7 +479,7 @@ let args_of_mconstr c = match kind_of_term c with
   | _ -> anomaly "args_of_mconstr called with bad args"
 
 let isMutConstruct c = match kind_of_term c with
-    IsMutCase _ -> true | _ -> false
+    IsMutConstruct _ -> true | _ -> false
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind_of_term c with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f2c7d0f14c..daef422981 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -985,7 +985,7 @@ let clenv_so_resolver allow_K clause gl =
 
 let clenv_unique_resolver allow_K clenv gls =
   let pathd,_ = whd_stack (clenv_instance_template_type clenv) in
-  let glhd,_ = whd_stack (pf_concl gls)in
+  let glhd,_ = whd_stack (pf_concl gls) in
   match kind_of_term pathd, kind_of_term glhd with
     | IsMeta _, IsLambda _ ->
 	(try 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 85ab52d1c5..7df546dc2a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -61,8 +61,8 @@ let rec prolog l n gl =
   let prol = (prolog l (n-1)) in
   (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
 
-let prolog_tac lcom n gl =
-  let l = List.map (pf_interp_constr gl) lcom in
+let prolog_tac l n gl =
+ (* let l = List.map (pf_interp_constr gl) lcom in *)
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
@@ -88,6 +88,8 @@ let instantiate n c gl =
 let instantiate_tac = function
   | [Integer n; Command com] ->
       (fun gl -> instantiate n (pf_interp_constr gl com) gl)
+  | [Integer n; Constr c] ->
+      (fun gl -> instantiate n c gl)
   | _ -> invalid_arg "Instantiate called with bad arguments"
 
 let whd_evar env sigma c = match kind_of_term c with
@@ -104,7 +106,7 @@ let normEvars gl =
 
 let vernac_prolog =
   let uncom = function
-    | Command com -> com
+    | Constr c -> c
     | _ -> assert false
   in
   let gentac = 
@@ -114,11 +116,10 @@ let vernac_prolog =
 	 | _ -> assert false)
   in 
   fun coms n -> 
-    gentac ((Integer n) :: (List.map (fun com -> (Command com)) coms))
+    gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
 
 let vernac_instantiate =
-  let gentac = hide_tactic "Instantiate" instantiate_tac in 
-  fun n com -> gentac [Integer n; Command com]
+  hide_tactic "Instantiate" instantiate_tac;;
 
 let vernac_normevars =
   hide_atomic_tactic "NormEvars" normEvars
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6363decfe1..b72aa80e1f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -488,7 +488,8 @@ let _ =
     (fun id_list () ->
        List.iter 
 	 (function 
-	    | VARG_CONSTANT sp -> Global.set_transparent sp
+(*	    | VARG_CONSTANT sp -> Global.set_transparent sp *)
+	    | VARG_QUALID sp -> Global.set_transparent sp
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
     
-- 
cgit v1.2.3