diff options
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/g_tactic.ml4 | 6 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 7 | ||||
-rw-r--r-- | plugins/ltac/tacentries.ml | 3 |
3 files changed, 9 insertions, 7 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index d792d4ff7..e68140828 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -115,10 +115,11 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map pi1 bl)) in + let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in (try List.index Names.Name.equal (snd x) ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = @@ -126,6 +127,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = user_err ~loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) @@ -160,7 +162,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e5ff47356..4f430b79e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) = let rec strip_ty acc n ty = match ty.CAst.v with Constrexpr.CProdN(bll,a) -> - let nb = - List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in - let bll = List.map (fun (x, _, y) -> x, y) bll in + let bll = List.map (function + | CLocalAssum (nal,_,t) -> nal,t + | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in + let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ee84be541..8112cc400 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -545,11 +545,10 @@ let print_located_tactic qid = (** Grammar *) let () = - let open Metasyntax in let entries = [ AnyEntry Pltac.tactic_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; AnyEntry Pltac.tactic_arg; ] in - register_grammar "tactic" entries + register_grammars_by_name "tactic" entries |