diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:45 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:45 +0000 |
commit | 1982377ee52a4361a3537f13f379facd6f57d62f (patch) | |
tree | f6d2d4b2ded81c5bca741b5250e96b49f6e5e294 /interp | |
parent | 88af5db4957e7e866ea507825ff0f08bd09c38ad (diff) |
Fixup implicits in patterns & notations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrextern.ml | 4 | ||||
-rw-r--r-- | interp/notation_ops.ml | 20 | ||||
-rw-r--r-- | interp/notation_ops.mli | 4 |
3 files changed, 14 insertions, 14 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5fec962b8..3c3858f29 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -423,7 +423,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = |Some true_args -> CPatCstr (loc, c, [], true_args) |None -> CPatCstr (loc, c, full_args, []) in insert_pat_alias loc p na -and apply_notation_to_pattern loc gr ((subst,substlist),more_args) +and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = function | NotationRule (sc,ntn) -> @@ -446,7 +446,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),more_args) let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in let l2' = if !Topconstr.oldfashion_patterns || ll <> [] then l2 else - match drop_implicits_in_patt gr (List.length l) l2 with + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 857e827a9..fb025be6f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -748,10 +748,10 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with - | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] - | PatVar (_,Anonymous), NHole _ -> sigma,[] + | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) + | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 -> - sigma,largs + sigma,(0,largs) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in @@ -761,21 +761,21 @@ let rec match_cases_pattern metas sigma a1 a2 = raise No_match else let l1',more_args = Util.list_chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) | r1, NList (x,_,iter,termin,lassoc) -> (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) - (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[] + (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - |out,[] -> out + |out,(_,[]) -> out |_ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with | NRef (IndRef r2) when ind = r2 -> - sigma,pats + sigma,(0,pats) | NApp (NRef (IndRef r2),l2) when ind = r2 -> let le2 = List.length l2 in @@ -784,7 +784,7 @@ let match_ind_pattern metas sigma ind pats a2 = raise No_match else let l1',more_args = Util.list_chop le2 pats in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) |_ -> raise No_match let reorder_canonically_substitution terms termlists metas = @@ -798,9 +798,9 @@ let reorder_canonically_substitution terms termlists metas = let match_notation_constr_cases_pattern c (metas,pat) = let vars = List.map fst metas in let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in - reorder_canonically_substitution terms termlists metas,more_args + reorder_canonically_substitution terms termlists metas, more_args let match_notation_constr_ind_pattern ind args (metas,pat) = let vars = List.map fst metas in let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in - reorder_canonically_substitution terms termlists metas,more_args + reorder_canonically_substitution terms termlists metas, more_args diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index ef92500f1..3389e4a3f 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -47,12 +47,12 @@ val match_notation_constr : bool -> glob_constr -> interpretation -> val match_notation_constr_cases_pattern : cases_pattern -> interpretation -> ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * - (cases_pattern list) + (int * cases_pattern list) val match_notation_constr_ind_pattern : inductive -> cases_pattern list -> interpretation -> ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * - (cases_pattern list) + (int * cases_pattern list) (** Substitution of kernel names in interpretation data *) |