aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml23
-rw-r--r--interp/constrintern.ml71
-rw-r--r--parsing/egrammar.ml12
-rw-r--r--parsing/egrammar.mli4
-rw-r--r--parsing/g_constrnew.ml44
-rw-r--r--parsing/g_vernacnew.ml42
-rw-r--r--parsing/lexer.ml496
-rw-r--r--parsing/lexer.mli8
-rw-r--r--toplevel/metasyntax.ml42
-rw-r--r--translate/ppconstrnew.ml17
-rw-r--r--translate/pptacticnew.ml6
-rw-r--r--translate/pptacticnew.mli2
12 files changed, 168 insertions, 119 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3eec91520..3fd4f121a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1131,13 +1131,18 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
let nparams =
(snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
- let params1 = list_tabulate (fun _ -> PatVar (loc,Anonymous)) nparams in
- (match params1@args1, a2 with
- | [], ARef (ConstructRef r2) when r1 = r2 -> sigma
- | l1, AApp (ARef (ConstructRef r2),l2)
- when r1 = r2 & List.length l1 = List.length l2 ->
- List.fold_left2 (match_cases_pattern metas) sigma l1 l2
- | _ -> raise No_match)
+ let l2 =
+ match a2 with
+ | ARef (ConstructRef r2) when r1 = r2 -> []
+ | AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2
+ | _ -> raise No_match in
+ if List.length l2 <> nparams + List.length args1
+ then raise No_match
+ else
+ let (p2,args2) = list_chop nparams l2 in
+ (* All parameters must be _ *)
+ List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+ List.fold_left2 (match_cases_pattern metas) sigma args1 args2
| _ -> raise No_match
let match_aconstr_cases_pattern c (metas_scl,pat) =
@@ -1205,8 +1210,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
insert_pat_delimiters (make_pat_notation loc ntn l) key)
| SynDefRule kn ->
CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn)))
- with
- No_match -> extern_symbol_pattern allscopes vars t rules
+ with
+ No_match -> extern_symbol_pattern allscopes vars t rules
(**********************************************************************)
(* Externalising applications *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 372ac0b7b..de5659c38 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -371,35 +371,53 @@ let subst_cases_pattern loc aliases intern subst scopes a =
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
- | ConstrPat of constructor
+ | ConstrPat of (constructor * cases_pattern list)
| VarPat of identifier
+let rec patt_of_rawterm loc cstr =
+ match cstr with
+ | RRef (_,(ConstructRef c as x)) ->
+ if !dump then add_glob loc x;
+ (c,[])
+ | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
+ | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
+ if !dump then add_glob loc x;
+ let (_,mib) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
+ let npar = mib.Declarations.mind_nparams in
+ let (params,args) =
+ if List.length pl <= npar then (pl,[]) else
+ list_chop npar pl in
+ (* All parameters must be _ *)
+ List.iter
+ (function RHole _ -> ()
+ | _ -> raise Not_found) params;
+ let pl' = List.map
+ (fun c ->
+ let (c,pl) = patt_of_rawterm loc c in
+ PatCstr(loc,c,pl,Anonymous)) args in
+ (c,pl')
+ | _ -> raise Not_found
+
let find_constructor ref =
let (loc,qid) = qualid_of_reference ref in
- try match extended_locate qid with
+ let gref =
+ try extended_locate qid
+ with Not_found ->
+ raise (InternalisationError (loc,NotAConstructor ref)) in
+ match gref with
| SyntacticDef sp ->
- (match Syntax_def.search_syntactic_definition loc sp with
- | RRef (_,(ConstructRef c as x)) ->
- if !dump then add_glob loc x;
- c
- | _ ->
- raise (InternalisationError (loc,NotAConstructor ref)))
+ let sdef = Syntax_def.search_syntactic_definition loc sp in
+ patt_of_rawterm loc sdef
| TrueGlobal r ->
let rec unf = function
| ConstRef cst ->
- (try
- let v = Environ.constant_value (Global.env()) cst in
- unf (reference_of_constr v)
- with
- Environ.NotEvaluableConst _ | Not_found ->
- raise (InternalisationError (loc,NotAConstructor ref)))
+ let v = Environ.constant_value (Global.env()) cst in
+ unf (reference_of_constr v)
| ConstructRef c ->
if !dump then add_glob loc r;
- c
- | _ -> raise (InternalisationError (loc,NotAConstructor ref))
+ c, []
+ | _ -> raise Not_found
in unf r
- with Not_found ->
- raise (InternalisationError (loc,NotAConstructor ref))
let find_pattern_variable = function
| Ident (loc,id) -> id
@@ -407,20 +425,27 @@ let find_pattern_variable = function
let maybe_constructor ref =
try ConstrPat (find_constructor ref)
- with InternalisationError _ -> VarPat (find_pattern_variable ref)
+ with
+ (* patt var does not exists globally *)
+ | InternalisationError _ -> VarPat (find_pattern_variable ref)
+ (* patt var also exists globally but does not satisfy preconditions *)
+ | (Environ.NotEvaluableConst _ | Not_found) ->
+ warn (str "pattern " ++ pr_reference ref ++
+ str " is understood as a pattern variable");
+ VarPat (find_pattern_variable ref)
let rec intern_cases_pattern scopes aliases tmp_scope = function
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
intern_cases_pattern scopes aliases' tmp_scope p
| CPatCstr (loc, head, pl) ->
- let c = find_constructor head in
+ let c,pl0 = find_constructor head in
let argscs =
simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
let (idsl,pl') =
List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl)
in
- (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases))
+ (aliases::(List.flatten idsl), PatCstr (loc,c,pl0@pl',alias_of aliases))
| CPatNotation (loc,"- _",[CPatNumeral(_,Bignat.POS p)]) ->
let scopes = option_cons tmp_scope scopes in
([aliases],
@@ -443,8 +468,8 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
aliases None e
| CPatAtom (loc, Some head) ->
(match maybe_constructor head with
- | ConstrPat c ->
- ([aliases], PatCstr (loc,c,[],alias_of aliases))
+ | ConstrPat (c,args) ->
+ ([aliases], PatCstr (loc,c,args,alias_of aliases))
| VarPat id ->
let aliases = merge_aliases aliases id in
([aliases], PatVar (loc,alias_of aliases)))
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 132dc7704..5880c0263 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -21,7 +21,9 @@ open Nameops
(* State of the grammar extensions *)
type all_grammar_command =
- | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
+ | Notation of
+ (int * Gramext.g_assoc option * notation * prod_item list *
+ int list option)
| Grammar of grammar_command
| TacticGrammar of
(string * (string * grammar_production list) * Tacexpr.raw_tactic_expr)
@@ -301,8 +303,12 @@ let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) =
let act = make_act ntl in
grammar_extend entry pos [(name, p4assoc, [symbs, act])]
-let extend_constr_notation (n,assoc,ntn,rule) =
- let mkact loc env = CNotation (loc,ntn,List.map snd env) in
+let extend_constr_notation (n,assoc,ntn,rule,permut) =
+ let mkact =
+ match permut with
+ None -> (fun loc env -> CNotation (loc,ntn,List.map snd env))
+ | Some p -> (fun loc env ->
+ CNotation (loc,ntn,List.map (fun i -> snd (List.nth env i)) p)) in
let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
let pos,p4assoc,name = find_position false keepassoc assoc level in
extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 362b9350a..e1f4dc6b1 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -18,7 +18,9 @@ open Rawterm
(*i*)
type all_grammar_command =
- | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
+ | Notation of
+ (int * Gramext.g_assoc option * notation * prod_item list *
+ int list option)
| Grammar of grammar_command
| TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 5ee178112..4cf3f25ab 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -304,7 +304,9 @@ GEXTEND Gram
[ r = Prim.reference -> CPatAtom (loc,Some r)
| "_" -> CPatAtom (loc,None)
| "("; p = pattern LEVEL "200"; ")" ->
- CPatNotation(loc,"( _ )",[p])
+ (match p with
+ CPatNumeral(_,Bignat.POS _) -> CPatNotation(loc,"( _ )",[p])
+ | _ -> p)
| n = INT -> CPatNumeral (loc,Bignat.POS(Bignat.of_string n)) ] ]
;
binder_list:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index e866d0172..cf89300bb 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -76,7 +76,7 @@ END
let test_plurial_form = function
- | [_] ->
+ | [(_,([_],_))] ->
Options.if_verbose warning
"Keywords Variables/Hypotheses/Parameters expect more than one assumption"
| _ -> ()
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 6424cb3d9..0a0228ac0 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -68,71 +68,64 @@ exception Error of error
let bad_token str = raise (Error (Bad_token str))
let check_special_token str =
- let rec loop = parser
+ let rec loop_symb = parser
| [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str
| [< _ = Stream.empty >] -> ()
- | [< '_ ; s >] -> loop s
+ | [< '_ ; s >] -> loop_symb s
in
- loop (Stream.of_string str)
+ loop_symb (Stream.of_string str)
let check_ident str =
- let rec loop = parser
- | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_'); s >] -> loop s
+ let first_letter = function
+ (''' | '0'..'9') -> false
+ | _ -> true in
+ let rec loop_id = parser
+ | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_'); s >] ->
+ loop_id s
(* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
- | [< ' ('\206' | '\207'); ' ('\128'..'\191'); s >] -> loop s
- (* iso 8859-1 accentuated letters *)
- | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255'); s >] -> loop s
+ | [< ' ('\206' | '\207'); ' ('\128'..'\191'); s >] -> loop_id s
+ | [< ''\226'; 'c2; 'c3; s >] ->
+ (match c2, c3 with
+ (* utf8 letter-like unicode 2100-214F *)
+ | (('\132', '\128'..'\191') | ('\133', '\128'..'\143')) ->
+ loop_id s
+ (* utf8 symbols (see [parse_226_tail]) *)
+ | (('\134'..'\143' | '\152'..'\155'
+ | '\164'..'\165' | '\168'..'\171'),_) ->
+ bad_token str
+ | _ -> (* default to iso 8859-1 "â" *)
+ if !Options.v7 then loop_id [< 'c2; 'c3; s >]
+ else bad_token str)
+ (* iso 8859-1 accentuated letters *)
+ | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255'); s >] ->
+ if !Options.v7 then loop_id s else bad_token str
| [< _ = Stream.empty >] -> ()
| [< >] -> bad_token str
in
- loop (Stream.of_string str)
+ if String.length str > 0 && first_letter str.[0] then
+ loop_id (Stream.of_string str)
+ else
+ bad_token str
-(* Special token dictionary *)
-let token_tree = ref empty_ttree
+let check_keyword str =
+ try check_special_token str
+ with Error _ -> check_ident str
-let add_special_token str =
- check_special_token str;
- token_tree := ttree_add !token_tree str
+(* Keyword and symbol dictionary *)
+let token_tree = ref empty_ttree
-(* Keyword identifier dictionary *)
-let keywords = ref empty_ttree
+let find_keyword s = ttree_find !token_tree s
-let find_keyword s = ttree_find !keywords s
+let is_keyword s =
+ try let _ = ttree_find !token_tree s in true with Not_found -> false
let add_keyword str =
- check_ident str;
- keywords := ttree_add !keywords str
-
-let is_keyword s =
- try let _ = ttree_find !keywords s in true with Not_found -> false
-
-let is_normal_token str =
- if String.length str > 0 then
- match str.[0] with
- | ' ' | '\n' | '\r' | '\t' | '"' -> bad_token str
- | '$' | 'a'..'z' | 'A'..'Z' | '_' -> true
- (* utf-8 symbols of the form "E2 xx xx" [E2=226] *)
- | '\226' when String.length str > 2 ->
- (match str.[1], str.[2] with
- | ('\132', '\128'..'\191') | ('\133', '\128'..'\143') ->
- (* utf8 letter-like unicode 2100-214F *) true
- | (('\134'..'\143' | '\152'..'\155'
- | '\164'..'\165' | '\168'..'\171'),_) ->
- (* utf8 symbols (see [parse_226_tail] *)
- false
- | _ ->
- (* default to iso 8859-1 "â" *)
- !Options.v7)
- (* iso 8859-1 accentuated letters *)
- | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' -> !Options.v7
- | _ -> false
- else
- bad_token str
+ check_keyword str;
+ token_tree := ttree_add !token_tree str
(* Adding a new token (keyword or special token). *)
let add_token (con, str) = match con with
- | "" ->
- if is_normal_token str then add_keyword str else add_special_token str
+ | "" -> add_keyword str
| "METAIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
-> ()
| _ ->
@@ -141,16 +134,15 @@ the constructor \"" ^ con ^ "\" is not recognized by Lexer"))
(* Freeze and unfreeze the state of the lexer *)
-type frozen_t = ttree * ttree
+type frozen_t = ttree
-let freeze () = (!keywords, !token_tree)
+let freeze () = !token_tree
-let unfreeze (kw,tt) =
- keywords := kw;
+let unfreeze tt =
token_tree := tt
let init () =
- unfreeze (empty_ttree, empty_ttree)
+ unfreeze empty_ttree
let _ = init()
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index b44e62eb9..b8004d58a 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -19,7 +19,7 @@ type error =
exception Error of error
-val add_keyword : string -> unit
+val add_token : string * string -> unit
val is_keyword : string -> bool
val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
@@ -31,11 +31,7 @@ val location_table : unit -> location_table
val restore_location_table : location_table -> unit
val check_ident : string -> unit
-val check_special_token : string -> unit
-
-val is_normal_token : string -> bool
-
-val add_token : Token.pattern -> unit
+val check_keyword : string -> unit
val tparse : string * string -> ((string * string) Stream.t -> string) option
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f5016c7d3..538c7563a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -357,15 +357,19 @@ let unquote_notation_token s =
let n = String.length s in
if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
+let is_normal_token str =
+ try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false
+
(* To protect alphabetic tokens and quotes from being seen as variables *)
let quote_notation_token x =
let n = String.length x in
- if (n > 0 & Lexer.is_normal_token x) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
+ let norm = is_normal_token x in
+ if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
else x
let rec analyse_notation_tokens = function
| [] -> [], []
- | String x :: sl when Lexer.is_normal_token x ->
+ | String x :: sl when is_normal_token x ->
Lexer.check_ident x;
let id = Names.id_of_string x in
let (vars,l) = analyse_notation_tokens sl in
@@ -373,7 +377,7 @@ let rec analyse_notation_tokens = function
error ("Variable "^x^" occurs more than once");
(id::vars, NonTerminal id :: l)
| String s :: sl ->
- Lexer.check_special_token s;
+ Lexer.check_keyword s;
let (vars,l) = analyse_notation_tokens sl in
(vars, Terminal (unquote_notation_token s) :: l)
| WhiteSpace n :: sl ->
@@ -629,10 +633,10 @@ let recompute_assoc typs =
| _, Some Gramext.RightA -> Some Gramext.RightA
| _ -> None
-let make_grammar_rule n typs symbols ntn =
+let make_grammar_rule n typs symbols ntn perm =
let assoc = recompute_assoc typs in
let prod = make_production typs symbols in
- (n,assoc,ntn,prod)
+ (n,assoc,ntn,prod, perm)
(* For old ast printer *)
let metas_of sl =
@@ -882,7 +886,7 @@ let add_syntax_extension local mv mv8 =
let prec,gram_rule = match data with
| None -> None, None
| Some ((_,_,notation),prec,(n,typs,symbols,_),_) ->
- Some prec, Some (make_grammar_rule n typs symbols notation) in
+ Some prec, Some (make_grammar_rule n typs symbols notation None) in
match data, data8 with
| None, None -> (* Nothing to do: V8Notation while not translating *) ()
| _, Some d | Some d, None ->
@@ -962,6 +966,17 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
let rule_name = ntn^"_"^scope_name^"_notation" in
make_syntax_rule n rule_name symbols typs ast ntn scope
+(* maps positions in v8-notation into positions in v7-notation (used
+ for parsing).
+ For instance Notation "x < y < z" := .. V8only "y < z < x"
+ yields [1; 2; 0] (y is the second arg in v7; z is 3rd; x is fst) *)
+let mk_permut vars7 vars8 =
+ if vars7=vars8 then None else
+ Some
+ (List.fold_right
+ (fun v8 subs -> list_index v8 vars7 - 1 :: subs)
+ vars8 [])
+
let add_notation_in_scope local df c mods omodv8 scope toks =
let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata),df') =
compute_syntax_data !Options.v7 (df,mods) in
@@ -974,32 +989,33 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
(* In short: parsing does not depend on omodv8 *)
(* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *)
(* if in v7, or of mods without scaling if in v8 *)
- let ppnot,ppprec,pp_rule =
+ let ppnot,ppvars,ppprec,pp_rule =
match omodv8 with
| Some mv8 ->
- let (_,_,ntn8),p,d,_ = compute_syntax_data false mv8 in
- ntn8,p,make_pp_rule d
+ let (_,vars8,ntn8),p,d,_ = compute_syntax_data false mv8 in
+ ntn8,vars8,p,make_pp_rule d
| _ ->
(* means the rule already exists: recover it *)
try
let _, oldprec8 = Symbols.level_of_notation notation in
let rule,_ = Symbols.find_notation_printing_rule notation in
- notation,oldprec8,rule
+ notation,vars,oldprec8,rule
with Not_found -> error "No known parsing rule for this notation in V8"
in
- let gram_rule = make_grammar_rule n typs symbols ppnot in
+ let permut = mk_permut vars ppvars in
+ let gram_rule = make_grammar_rule n typs symbols ppnot permut in
Lib.add_anonymous_leaf
(inSyntaxExtension
(local,(Some prec,ppprec),ppnot,Some gram_rule,pp_rule));
(* Declare interpretation *)
- let a = interp_aconstr [] vars c in
+ let a = interp_aconstr [] ppvars c in
let old_pp_rule =
(* Used only by v7 *)
if onlyparse then None
else
let r = interp_global_rawconstr_with_vars vars c in
- Some (make_old_pp_rule n symbols typs r notation scope vars) in
+ Some (make_old_pp_rule n symbols typs r ppnot scope vars) in
let onlyparse = onlyparse or !Options.v7_only in
let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
Lib.add_anonymous_leaf
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 1da57f920..8a2ce3765 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -262,11 +262,14 @@ let split_product na' = function
rename na na' t (CProdN(loc,(nal,t)::bl,c))
| _ -> anomaly "ill-formed fixpoint body"
-let merge_binders (na1,ty1) (na2,ty2) =
+let merge_binders (na1,ty1) (na2,ty2) codom =
let na =
match snd na1, snd na2 with
Anonymous, Name id -> na2
- | Name id, Anonymous -> na1
+ | Name id, Anonymous ->
+ if occur_var_constr_expr id codom then
+ failwith "avoid capture"
+ else na1
| Anonymous, Anonymous -> na1
| Name id1, Name id2 ->
if id1 <> id2 then failwith "not same name" else na1 in
@@ -277,18 +280,18 @@ let merge_binders (na1,ty1) (na2,ty2) =
| _ ->
Constrextern.check_same_type ty1 ty2;
ty2 in
- LocalRawAssum ([na],ty)
+ (LocalRawAssum ([na],ty), codom)
let rec strip_domain bvar c =
match c with
| CArrow(loc,a,b) ->
- (merge_binders bvar ((dummy_loc,Anonymous),a), b)
+ merge_binders bvar ((dummy_loc,Anonymous),a) b
| CProdN(loc,[([na],ty)],c') ->
- (merge_binders bvar (na,ty), c')
+ merge_binders bvar (na,ty) c'
| CProdN(loc,([na],ty)::bl,c') ->
- (merge_binders bvar (na,ty), CProdN(loc,bl,c'))
+ merge_binders bvar (na,ty) (CProdN(loc,bl,c'))
| CProdN(loc,(na::nal,ty)::bl,c') ->
- (merge_binders bvar (na,ty), CProdN(loc,(nal,ty)::bl,c'))
+ merge_binders bvar (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
| _ -> failwith "not a product"
(* Note: binder sharing is lost *)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b4002994f..63423b7b5 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -145,7 +145,7 @@ let id_of_ltac_v7_id id =
let pr_ltac_or_var pr = function
| ArgArg x -> pr x
| ArgVar (loc,id) ->
- pr_with_comments loc (Nameops.pr_id (id_of_ltac_v7_id id))
+ pr_with_comments loc (pr_id (id_of_ltac_v7_id id))
let pr_arg pr x = spc () ++ pr x
@@ -331,9 +331,9 @@ let pr_seq_body pr tl =
let duplicate force pr = function
| [] -> pr (ref false,[])
- | [x] -> pr x
+ | x::l when List.for_all (fun y -> snd x=snd y) l -> pr x
| l ->
- if List.exists (fun (b,ids) -> !b) l & (force or
+ if List.exists (fun (b,ids) -> !b) l & (force or
List.exists (fun (_,ids) -> ids <> (snd (List.hd l))) (List.tl l))
then pr_seq_body pr (List.rev l)
else pr (ref false,[])
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index b6861f816..88f57f61a 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -24,3 +24,5 @@ val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds
val id_of_ltac_v7_id : identifier -> identifier
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 16:27:30 +0000