From f61e682857596f0274b956295efd2bfba63bc8c0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 18 Dec 2012 07:01:07 +0000 Subject: Fixing parsing of specific primitive tokens used as notations for patterns (e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrexpr_ops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 602c2314a..e9dae6421 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -345,5 +345,5 @@ let rec raw_cases_pattern_expr_of_glob_constr looked_for = function RCPatCstr (loc, g,[],[]) | GApp (loc,GRef (_,g),l) -> looked_for g; - RCPatCstr (loc, g,[],List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l) + RCPatCstr (loc, g,List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l,[]) | _ -> raise Not_found -- cgit v1.2.3