diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 6 | ||||
| -rw-r--r-- | interp/constrextern.ml | 11 | ||||
| -rw-r--r-- | interp/constrintern.ml | 14 |
3 files changed, 18 insertions, 13 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ca36f4c9f8..01efef9408 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -149,10 +149,10 @@ let rec constr_expr_eq e1 e2 = constr_expr_eq t1 t2 && constr_expr_eq f1 f2 | CHole _, CHole _ -> true - | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) -> - (b1 : bool) == b2 && Id.equal i1 i2 + | CPatVar(_,i1), CPatVar(_,i2) -> + Id.equal i1 i2 | CEvar (_, id1, c1), CEvar (_, id2, c2) -> - Id.equal id1 id2 && Option.equal (List.equal instance_eq) c1 c2 + Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort(_,s1), CSort(_,s2) -> Miscops.glob_sort_eq s1 s2 | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9a6f8b22cd..f71cf5a65b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -671,13 +671,14 @@ let rec extern inctx scopes vars r = | GVar (loc,id) -> CRef (Ident (loc,id),None) - | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None) + | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, None) | GEvar (loc,n,l) -> - extern_evar loc n (Option.map (List.map (on_snd (extern false scopes vars))) l) + extern_evar loc n (List.map (on_snd (extern false scopes vars)) l) - | GPatVar (loc,n) -> - if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n) + | GPatVar (loc,(b,n)) -> + if !print_meta_as_hole then CHole (loc, None, None) else + if b then CPatVar (loc,n) else CEvar (loc,n,[]) | GApp (loc,f,args) -> (match f with @@ -1030,7 +1031,7 @@ let rec glob_of_pat env sigma = function let test id = function PVar id' -> Id.equal id id' | _ -> false in let l = Evd.evar_instance_array test (Evd.find sigma evk) l in let id = Evd.evar_ident evk sigma in - GEvar (loc,id,Some (List.map (on_snd (glob_of_pat env sigma)) l)) + GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ff96340cde..d020a51535 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1579,14 +1579,18 @@ let internalize globalenv env allow_patvar lvar c = Some glb in GHole (loc, k, solve) + (* Parsing pattern variables *) | CPatVar (loc, n) when allow_patvar -> - GPatVar (loc, n) - | CPatVar (loc, (false,n)) -> - GEvar (loc, n, None) + GPatVar (loc, (true,n)) + | CEvar (loc, n, []) when allow_patvar -> + GPatVar (loc, (false,n)) + (* end *) + (* Parsing existential variables *) + | CEvar (loc, n, l) -> + GEvar (loc, n, List.map (on_snd (intern env)) l) | CPatVar (loc, _) -> raise (InternalizationError (loc,IllegalMetavariable)) - | CEvar (loc, n, l) -> - GEvar (loc, n, Option.map (List.map (on_snd (intern env))) l) + (* end *) | CSort (loc, s) -> GSort(loc,s) | CCast (loc, c1, c2) -> |