diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8e876ec16d..33b93606ec 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -690,7 +690,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig | { CAst.v = GVar id' } -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable") + | _ -> anomaly (str "A term which can be a binder has to be a variable.") with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) @@ -830,7 +830,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in add_bindinglist_env sigma var bl with Not_found -> - anomaly (str "There should be a binder list bindings this list of terms") + anomaly (str "There should be a binder list bindings this list of terms.") let match_fix_kind fk1 fk2 = match (fk1,fk2) with @@ -1154,10 +1154,6 @@ let match_notation_constr u c (metas,pat) = metas ([],[],[]) (* Matching cases pattern *) -let add_patterns_for_params ind l = - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = try @@ -1187,10 +1183,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,add_patterns_for_params (fst r1) largs) + let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + sigma,(0,l) | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in + let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then |