diff options
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 13 | ||||
| -rw-r--r-- | 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) |