diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-16 23:59:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-07 15:27:41 +0200 |
| commit | f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf (patch) | |
| tree | af78db19a74445cb5a2000a7947f2e806e01e78c /interp/notation_ops.ml | |
| parent | 495bccc436cfe72af9955b4b9d8564a8831850b9 (diff) | |
Better support for printing constructors with let-ins.
This allows e.g. to use the record notations even when there are
defined fields.
A priori fixed also missing parameters when interpreting primitive
tokens.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0c5393cf4..564882153 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1158,6 +1158,7 @@ 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 @@ -1190,10 +1191,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 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(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 (loc,(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 |