diff options
| author | pboutill | 2012-02-29 13:43:00 +0000 |
|---|---|---|
| committer | pboutill | 2012-02-29 13:43:00 +0000 |
| commit | fa7e4e07bc9bf6b2b36667bf3531735f0c810abc (patch) | |
| tree | 2e561fb1d258ad09c7739810c6344973d3794e6b | |
| parent | 457bf8fee3b53b8306d0dcdf49e637c29592d6c3 (diff) | |
Fix compilation of Constrintern...
I love being push under presure to commit and do not try my fixup !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 06202bc9e5..04e252ca37 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1586,17 +1586,17 @@ let internalize sigma globalenv env allow_patvar lvar c = let (match_to_do,nal) = let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc = let add_name l = function - |Anonymous -> l - |Name y -> (y,PatVar(loc,x)) :: l in + |_,Anonymous -> l + |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) |(_,Some _,_)::t, l -> canonize_args t l forbidden_names match_acc var_acc |[],[] -> - (add_name match_acc (snd na), var_acc) + (add_name match_acc na, var_acc) |_::t,PatVar (loc,x)::tt -> canonize_args t tt forbidden_names - (add_name match_acc x) ((loc,x)::var_acc) + (add_name match_acc (loc,x)) ((loc,x)::var_acc) |(cano_name,_,ty)::t,c::tt -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in |