diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 67fee62028..c9fc3aa4f3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -664,11 +664,11 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in - let (loc,(na,bk,t)) = a in + let (_loc,(na,bk,t)) = a in CAst.make ?loc @@ GProd (na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in - let (loc,(na,bk,t)) = a in + let (_loc,(na,bk,t)) = a in CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') @@ -1219,6 +1219,11 @@ let alias_of als = match als.alias_ids with *) +let is_zero s = + let rec aux i = + Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) + in aux 0 + let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1331,9 +1336,9 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[]) - when Bigint.is_strictly_pos p -> - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in + | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[]) + when not (is_zero p) -> + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in rcp_of_glob pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a @@ -1639,9 +1644,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = CAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[])) - when Bigint.is_strictly_pos p -> - intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p))) + | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[])) + when not (is_zero p) -> + intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) | CNotation ("( _ )",([a],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args |