diff options
| author | herbelin | 2004-02-03 15:58:53 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-03 15:58:53 +0000 |
| commit | 01e3bb129c470745ea5d45ab17a392b6b962e650 (patch) | |
| tree | 214dbf3591faa9627607f4f801681d76238a0bc2 /interp | |
| parent | 48179af6722ff28634db711b26cd461391765681 (diff) | |
Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un nom doit filtrer un nom et anonymous doit filtrer anonymous
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1e8a10a874..cc9488a3e3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -286,17 +286,12 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | _,_ -> raise No_match and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with - | (na1,Name id2) when List.mem id2 metas -> - let sigma = - name_fold - (fun id sigma -> bind_env sigma id2 (RVar (dummy_loc,id))) na1 sigma - in - match_ alp metas sigma b1 b2 - | (na1,na2) -> - let alp = - name_fold - (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in + | (Name id1,Name id2) when List.mem id2 metas -> + let sigma = bind_env sigma id2 (RVar (dummy_loc,id1)) in match_ alp metas sigma b1 b2 + | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2 + | (Anonymous,Anonymous) -> match_ alp metas sigma b1 b2 + | _ -> raise No_match and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then |