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 --- tactics/eauto.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'tactics/eauto.ml') diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 85ab52d1c..7df546dc2 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 -- cgit v1.2.3