diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8b457ab37b..3d29da025e 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (qid,_) when qualid_is_ident qid -> found c.CAst.loc (qualid_basename qid) bdvars l - | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c @@ -203,8 +203,9 @@ let warn_ignoring_implicit_status = let implicits_of_glob_constr ?(with_products=true) l = let add_impl ?loc na bk l = match bk with - | Implicit -> CAst.make ?loc (Some (na,true)) :: l - | _ -> CAst.make ?loc None :: l + | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l + | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l + | Explicit -> CAst.make ?loc None :: l in let rec aux c = match DAst.get c with @@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then add_impl na bk (aux b) else let () = match bk with - | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc - | _ -> () + | NonMaxImplicit + | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | Explicit -> () in [] | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) | GLetIn (na, b, t, c) -> aux c |